src/Pure/Proof/reconstruct.ML

--- a/src/Pure/Proof/reconstruct.ML	Tue Mar 30 12:47:39 2010 +0200
+++ b/src/Pure/Proof/reconstruct.ML	Tue Mar 30 15:25:30 2010 +0200
@@ -136,8 +136,8 @@
 
     fun mk_cnstrts_atom env vTs prop opTs prf =
           let
-            val tvars = OldTerm.term_tvars prop;
-            val tfrees = OldTerm.term_tfrees prop;
+            val tvars = Term.add_tvars prop [] |> rev;
+            val tfrees = Term.add_tfrees prop [] |> rev;
             val (Ts, env') =
               (case opTs of
                 NONE => fold_map mk_tvar (map snd tvars @ map snd tfrees) env
@@ -304,7 +304,7 @@
   end;
 
 fun prop_of_atom prop Ts = subst_atomic_types
-  (map TVar (OldTerm.term_tvars prop) @ map TFree (OldTerm.term_tfrees prop) ~~ Ts)
+  (map TVar (Term.add_tvars prop [] |> rev) @ map TFree (Term.add_tfrees prop [] |> rev) ~~ Ts)
   (forall_intr_vfs prop);
 
 val head_norm = Envir.head_norm (Envir.empty 0);
@@ -370,9 +370,9 @@
                   end
               | SOME (maxidx', prf) => (maxidx' + maxidx + 1,
                   incr_indexes (maxidx + 1) prf, prfs));
-            val tfrees = OldTerm.term_tfrees prop;
+            val tfrees = Term.add_tfrees prop [] |> rev;
             val tye = map (fn ((s, j), _) => (s, maxidx + 1 + j))
-              (OldTerm.term_tvars prop) @ map (rpair ~1 o fst) tfrees ~~ Ts;
+              (Term.add_tvars prop [] |> rev) @ map (rpair ~1 o fst) tfrees ~~ Ts;
             val varify = map_type_tfree (fn p as (a, S) =>
               if member (op =) tfrees p then TVar ((a, ~1), S) else TFree p)
           in