diff -r 1b9db2581fe2 -r d6c91bc3e49c src/Pure/pattern.ML
--- a/src/Pure/pattern.ML	Mon Dec 17 14:27:18 2001 +0100
+++ b/src/Pure/pattern.ML	Tue Dec 18 02:17:20 2001 +0100
@@ -183,7 +183,7 @@
 
 fun unify_types(T,U, env as Envir.Envir{asol,iTs,maxidx}) =
   if T=U then env
-  else let val (iTs',maxidx') = Type.unify (!tsgr) maxidx iTs (U,T)
+  else let val (iTs',maxidx') = Type.unify (!tsgr) (iTs, maxidx) (U, T)
        in Envir.Envir{asol=asol,maxidx=maxidx',iTs=iTs'} end
        handle Type.TUNIFY => raise Unif;