diff -r 91ded127f5f7 -r 9ef19e3c7fdd src/Pure/Proof/reconstruct.ML
--- a/src/Pure/Proof/reconstruct.ML	Thu Jul 28 15:19:48 2005 +0200
+++ b/src/Pure/Proof/reconstruct.ML	Thu Jul 28 15:19:49 2005 +0200
@@ -62,7 +62,7 @@
 fun unifyT sg env T U =
   let
     val Envir.Envir {asol, iTs, maxidx} = env;
-    val (iTs', maxidx') = Type.unify (Sign.tsig_of sg) (iTs, maxidx) (T, U)
+    val (iTs', maxidx') = Sign.typ_unify sg (T, U) (iTs, maxidx)
   in Envir.Envir {asol=asol, iTs=iTs', maxidx=maxidx'} end
   handle Type.TUNIFY => error ("Non-unifiable types:\n" ^
     Sign.string_of_typ sg T ^ "\n\n" ^ Sign.string_of_typ sg U);