src/Pure/unify.ML
changeset 1435 aefcd255ed4a
parent 922 196ca0973a6d
child 1458 fd510875fb71
--- a/src/Pure/unify.ML	Tue Jan 09 13:45:58 1996 +0100
+++ b/src/Pure/unify.ML	Thu Jan 11 10:29:31 1996 +0100
@@ -242,10 +242,11 @@
 
 
 fun unify_types(T,U, env as Envir.Envir{asol,iTs,maxidx}) =
-	if T=U then env else
-	let val iTs' = Sign.Type.unify (#tsig(Sign.rep_sg (!sgr))) ((U,T),iTs)
-	in Envir.Envir{asol=asol,maxidx=maxidx,iTs=iTs'}
-	end handle Sign.Type.TUNIFY => raise CANTUNIFY;
+  if T=U then env
+  else let val (iTs',maxidx') = Sign.Type.unify (#tsig(Sign.rep_sg (!sgr)))
+                                                maxidx iTs (U,T)
+       in Envir.Envir{asol=asol,maxidx=maxidx',iTs=iTs'} end
+       handle Sign.Type.TUNIFY => raise CANTUNIFY;
 
 fun test_unify_types(args as (T,U,_)) =
 let val sot = Sign.string_of_typ (!sgr);