Type_Infer.finish: index 0 -- freshness supposedly via Name.invents;
Type_Infer.fixate_params: full Proof.context;

--- a/src/Pure/Isar/proof_context.ML	Mon Sep 13 11:35:55 2010 +0200
+++ b/src/Pure/Isar/proof_context.ML	Mon Sep 13 12:42:08 2010 +0200
@@ -599,7 +599,7 @@
 
 fun prepare_patterns ctxt =
   let val Mode {pattern, ...} = get_mode ctxt in
-    Type_Infer.fixate_params (Variable.names_of ctxt) #>
+    Type_Infer.fixate_params ctxt #>
     pattern ? Variable.polymorphic ctxt #>
     (map o Term.map_types) (prepare_patternT ctxt) #>
     (if pattern then prepare_dummies else map (check_dummies ctxt))

--- a/src/Pure/type_infer.ML	Mon Sep 13 11:35:55 2010 +0200
+++ b/src/Pure/type_infer.ML	Mon Sep 13 12:42:08 2010 +0200
@@ -12,7 +12,7 @@
   val param: int -> string * sort -> typ
   val paramify_vars: typ -> typ
   val paramify_dummies: typ -> int -> typ * int
-  val fixate_params: Name.context -> term list -> term list
+  val fixate_params: Proof.context -> term list -> term list
   val infer_types: Proof.context -> (string -> typ option) -> (indexname -> typ option) ->
     term list -> term list
 end;
@@ -54,7 +54,7 @@
       | paramify T maxidx = (T, maxidx);
   in paramify end;
 
-fun fixate_params name_context ts =
+fun fixate_params ctxt ts =
   let
     fun subst_param (xi, S) (inst, used) =
       if is_param xi then
@@ -63,8 +63,8 @@
           val used' = Name.declare a used;
         in (((xi, S), TFree (a, S)) :: inst, used') end
       else (inst, used);
-    val name_context' = (fold o fold_types) Term.declare_typ_names ts name_context;
-    val (inst, _) = fold_rev subst_param (fold Term.add_tvars ts []) ([], name_context');
+    val used = (fold o fold_types) Term.declare_typ_names ts (Variable.names_of ctxt);
+    val (inst, _) = fold_rev subst_param (fold Term.add_tvars ts []) ([], used);
   in (map o map_types) (Term_Subst.instantiateT inst) ts end;
 
 
@@ -188,7 +188,6 @@
     val parms = rev ((fold o fold_types) (add_parms tye) ts (fold (add_parms tye) Ts []));
     val names = Name.invents used ("?" ^ Name.aT) (length parms);
     val tab = Vartab.make (parms ~~ names);
-    val idx = Variable.maxidx_of ctxt + 1;
 
     fun finish_typ T =
       (case deref tye T of
@@ -197,7 +196,7 @@
       | U as TVar (xi, S) =>
           (case Vartab.lookup tab xi of
             NONE => U
-          | SOME a => TVar ((a, idx), S)));
+          | SOME a => TVar ((a, 0), S)));
   in (map finish_typ Ts, map (Type.strip_constraints o Term.map_types finish_typ) ts) end;