tuned;

--- 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;