avoid clones of Isabelle/ML operations --- de-emphasize somewhat old/outdated operation;