src/Pure/pattern.ML
changeset 1435 aefcd255ed4a
parent 1029 27808dabf4af
child 1458 fd510875fb71
     1.1 --- a/src/Pure/pattern.ML	Tue Jan 09 13:45:58 1996 +0100
     1.2 +++ b/src/Pure/pattern.ML	Thu Jan 11 10:29:31 1996 +0100
     1.3 @@ -184,8 +184,8 @@
     1.4  
     1.5  fun unify_types(T,U, env as Envir.Envir{asol,iTs,maxidx}) =
     1.6    if T=U then env
     1.7 -  else let val iTs' = Type.unify (!tsgr) ((U,T),iTs)
     1.8 -       in Envir.Envir{asol=asol,maxidx=maxidx,iTs=iTs'} end
     1.9 +  else let val (iTs',maxidx') = Type.unify (!tsgr) maxidx iTs (U,T)
    1.10 +       in Envir.Envir{asol=asol,maxidx=maxidx',iTs=iTs'} end
    1.11         handle Type.TUNIFY => raise Unif;
    1.12  
    1.13  fun unif binders (env,(s,t)) = case (devar env s,devar env t) of