# HG changeset patch # User wenzelm # Date 1570544239 -7200 # Node ID 58677c92bef74764aa08789a21ac51846763836e # Parent d5ffda5a3cdaf599cb4581ddfad4baa8d0d21517 tuned; diff -r d5ffda5a3cda -r 58677c92bef7 src/Pure/proofterm.ML --- a/src/Pure/proofterm.ML Tue Oct 08 16:11:04 2019 +0200 +++ b/src/Pure/proofterm.ML Tue Oct 08 16:17:19 2019 +0200 @@ -1080,6 +1080,7 @@ fun vars_of t = map Var (rev (Term.add_vars t [])); fun frees_of t = map Free (rev (Term.add_frees t [])); +fun variables_of t = vars_of t @ frees_of t; fun test_args _ [] = true | test_args is (Bound i :: ts) = @@ -1567,10 +1568,6 @@ exception MIN_PROOF of unit; -fun vars_of t = map Var (rev (Term.add_vars t [])); -fun frees_of t = map Free (rev (Term.add_frees t [])); -fun variables_of t = vars_of t @ frees_of t; - fun forall_intr_vfs prop = fold_rev Logic.all (variables_of prop) prop; fun forall_intr_vfs_prf prop prf = fold_rev forall_intr_proof' (variables_of prop) prf;