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