src/Pure/proofterm.ML

--- a/src/Pure/proofterm.ML	Sat Nov 15 21:31:37 2008 +0100
+++ b/src/Pure/proofterm.ML	Sun Nov 16 18:18:45 2008 +0100
@@ -837,7 +837,8 @@
 
 val proofs = ref 2;
 
-fun vars_of t = rev (fold_aterms (fn v as Var _ => insert (op =) v | _ => I) t []);
+fun vars_of t = map Var (rev (Term.add_vars t []));
+fun frees_of t = map Free (rev (Term.add_frees t []));
 
 fun test_args _ [] = true
   | test_args is (Bound i :: ts) =
@@ -895,7 +896,7 @@
     val nvs = needed_vars prop;
     val args = map (fn (v as Var (ixn, _)) =>
         if member (op =) nvs ixn then SOME v else NONE) (vars_of prop) @
-      map SOME (sort Term.term_ord (term_frees prop));
+      map SOME (frees_of prop);
   in
     proof_combt' (c (name, prop, NONE), args)
   end;
@@ -1218,7 +1219,7 @@
     val nvs = needed_vars prop;
     val args = map (fn (v as Var (ixn, _)) =>
         if member (op =) nvs ixn then SOME v else NONE) (vars_of prop) @
-      map SOME (sort Term.term_ord (term_frees prop));
+      map SOME (frees_of prop);
 
     val proof0 =
       if ! proofs = 2 then