# HG changeset patch
# User wenzelm
# Date 1303202258 -7200
# Node ID 26c8c9cabb2436784ae8b89447f916aae6bdd71a
# Parent  95b17b4901b562f6916b60fc4bc307f3325a8598
more precise treatment of existing type inference parameters;
tuned;

diff -r 95b17b4901b5 -r 26c8c9cabb24 src/Pure/type_infer.ML
--- a/src/Pure/type_infer.ML	Mon Apr 18 23:41:15 2011 +0200
+++ b/src/Pure/type_infer.ML	Tue Apr 19 10:37:38 2011 +0200
@@ -8,6 +8,8 @@
 sig
   val is_param: indexname -> bool
   val is_paramT: typ -> bool
+  val param_maxidx: term -> int -> int
+  val param_maxidx_of: term list -> int
   val param: int -> string * sort -> typ
   val mk_param: int -> sort -> typ
   val anyT: sort -> typ
@@ -34,6 +36,12 @@
 fun is_paramT (TVar (xi, _)) = is_param xi
   | is_paramT _ = false;
 
+val param_maxidx =
+  (Term.fold_types o Term.fold_atyps)
+    (fn (TVar (xi as (_, i), _)) => if is_param xi then Integer.max i else I | _ => I);
+
+fun param_maxidx_of ts = fold param_maxidx ts ~1;
+
 fun param i (x, S) = TVar (("?" ^ x, i), S);
 
 fun mk_param i S = TVar (("?'a", i), S);
@@ -69,7 +77,7 @@
 fun prepare_typ typ params_idx =
   let
     val (params', idx) = fold_atyps
-      (fn TVar (xi as (x, _), S) =>
+      (fn TVar (xi, S) =>
           (fn ps_idx as (ps, idx) =>
             if is_param xi andalso not (Vartab.defined ps xi)
             then (Vartab.update (xi, mk_param idx S) ps, idx + 1) else ps_idx)
@@ -160,7 +168,7 @@
       (case Vartab.lookup tye xi of
         NONE => T
       | SOME U => deref tye U)
-  | deref tye T = T;
+  | deref _ T = T;
 
 fun add_parms tye T =
   (case deref tye T of
@@ -247,7 +255,7 @@
 
     (* occurs check and assignment *)
 
-    fun occurs_check tye xi (TVar (xi', S)) =
+    fun occurs_check tye xi (TVar (xi', _)) =
           if xi = xi' then raise NO_UNIFIER ("Occurs check!", tye)
           else
             (case Vartab.lookup tye xi' of
@@ -343,10 +351,11 @@
         | t => t);
 
     val ts = burrow_types (Syntax.check_typs ctxt) raw_ts;
-    val (ts', (_, _, idx)) =
+    val idx = param_maxidx_of ts + 1;
+    val (ts', (_, _, idx')) =
       fold_map (prepare_term ctxt const_type o constrain_vars) ts
-        (Vartab.empty, Vartab.empty, 0);
-  in (idx, ts') end;
+        (Vartab.empty, Vartab.empty, idx);
+  in (idx', ts') end;
 
 fun infer_types ctxt const_type var_type raw_ts =
   let