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