src/Pure/Proof/reconstruct.ML

--- a/src/Pure/Proof/reconstruct.ML	Tue Oct 31 09:29:01 2006 +0100
+++ b/src/Pure/Proof/reconstruct.ML	Tue Oct 31 09:29:06 2006 +0100
@@ -144,7 +144,7 @@
           let
             val tvars = term_tvars prop;
             val tfrees = term_tfrees prop;
-            val (prop', fmap) = Type.varify (prop, []);
+            val (fmap, prop') = Type.varify [] prop;
             val (env', Ts) = (case opTs of
                 NONE => foldl_map mk_tvar (env, map snd tvars @ map snd tfrees)
               | SOME Ts => (env, Ts));
@@ -306,7 +306,7 @@
   end;
 
 fun prop_of_atom prop Ts =
-  let val (prop', fmap) = Type.varify (prop, []);
+  let val (fmap, prop') = Type.varify [] prop;
   in subst_TVars (map fst (term_tvars prop) @ map snd fmap ~~ Ts)
     (forall_intr_vfs prop')
   end;