src/Pure/unify.ML

 exception ASSIGN;	(*Raised if not an assignment*)
 
 
 fun unify_types thy (T,U, env as Envir.Envir{asol,iTs,maxidx}) =
   if T=U then env
-  else let val (iTs',maxidx') = Type.unify (Sign.tsig_of thy) (iTs, maxidx) (U, T)
+  else let val (iTs',maxidx') = Sign.typ_unify thy (U, T) (iTs, maxidx)
        in Envir.Envir{asol=asol,maxidx=maxidx',iTs=iTs'} end
        handle Type.TUNIFY => raise CANTUNIFY;
 
 fun test_unify_types thy (args as (T,U,_)) =
 let val str_of = Sign.string_of_typ thy;