diff --git a/generic/proof-script.el b/generic/proof-script.el index 31e5d083b..d4e26405c 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -2736,7 +2736,7 @@ with something different." (eq typ 'proverproc) (eq typ 'proof) (and proof-ignore-for-undo-count cmd - (proof-string-match proof-ignore-for-undo-count cmd)))) + (proof-stringfn-match proof-ignore-for-undo-count cmd)))) ;; some named element: use generic forget-id function; finish. ((setq name (span-property span 'name)) (setq ans (format proof-forget-id-command name))