tuned Type.unify;

--- a/src/HOL/Tools/inductive_package.ML	Mon Dec 17 14:27:18 2001 +0100
+++ b/src/HOL/Tools/inductive_package.ML	Tue Dec 18 02:17:20 2001 +0100
@@ -190,7 +190,7 @@
     val intr_consts = foldl add_term_consts_2 ([], intr_ts');
     fun unify (env, (cname, cT)) =
       let val consts = map snd (filter (fn c => fst c = cname) intr_consts)
-      in foldl (fn ((env', j'), Tp) => (Type.unify tsig j' env' Tp))
+      in foldl (fn ((env', j'), Tp) => (Type.unify tsig (env', j') Tp))
           (env, (replicate (length consts) cT) ~~ consts)
       end;
     val (env, _) = foldl unify ((Vartab.empty, i'), rec_consts);

--- a/src/Pure/Proof/reconstruct.ML	Mon Dec 17 14:27:18 2001 +0100
+++ b/src/Pure/Proof/reconstruct.ML	Tue Dec 18 02:17:20 2001 +0100
@@ -97,7 +97,7 @@
 fun unifyT sg env T U =
   let
     val Envir.Envir {asol, iTs, maxidx} = env;
-    val (iTs', maxidx') = Type.unify (Sign.tsig_of sg) maxidx iTs (T, U)
+    val (iTs', maxidx') = Type.unify (Sign.tsig_of sg) (iTs, maxidx) (T, U)
   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);

--- a/src/Pure/drule.ML	Mon Dec 17 14:27:18 2001 +0100
+++ b/src/Pure/drule.ML	Tue Dec 18 02:17:20 2001 +0100
@@ -706,7 +706,7 @@
         and {sign=signu, t=u, T= U, maxidx=maxu,...} = rep_cterm cu;
         val maxi = Int.max(maxidx, Int.max(maxt, maxu));
         val sign' = Sign.merge(sign, Sign.merge(signt, signu))
-        val (tye',maxi') = Type.unify (#tsig(Sign.rep_sg sign')) maxi tye (T,U)
+        val (tye',maxi') = Type.unify (#tsig(Sign.rep_sg sign')) (tye, maxi) (T, U)
           handle Type.TUNIFY => raise TYPE("Ill-typed instantiation", [T,U], [t,u])
     in  (sign', tye', maxi')  end;
 in

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

--- a/src/Pure/unify.ML	Mon Dec 17 14:27:18 2001 +0100
+++ b/src/Pure/unify.ML	Tue Dec 18 02:17:20 2001 +0100
@@ -179,8 +179,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 (#tsig(Sign.rep_sg (!sgr)))
-                                                maxidx iTs (U,T)
+  else let val (iTs',maxidx') = Type.unify (#tsig(Sign.rep_sg (!sgr))) (iTs, maxidx) (U, T)
        in Envir.Envir{asol=asol,maxidx=maxidx',iTs=iTs'} end
        handle Type.TUNIFY => raise CANTUNIFY;