Frees in PThms are now quantified in the order of their appearance in the
proposition as well, to make it compatible (again) with variable order used
by forall_intr_frees.

--- a/src/Pure/Proof/extraction.ML	Sat Nov 15 21:31:37 2008 +0100
+++ b/src/Pure/Proof/extraction.ML	Sun Nov 16 18:18:45 2008 +0100
@@ -125,8 +125,9 @@
 
 fun msg d s = priority (Symbol.spaces d ^ s);
 
-fun vars_of t = rev (fold_aterms (fn v as Var _ => insert (op =) v | _ => I) t []);
-fun vfs_of t = vars_of t @ sort Term.term_ord (term_frees t);
+fun vars_of t = map Var (rev (Term.add_vars t []));
+fun frees_of t = map Free (rev (Term.add_frees t []));
+fun vfs_of t = vars_of t @ frees_of t;
 
 fun forall_intr_prf (t, prf) =
   let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p)

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