load type_infer.ML later -- proper context for Type_Infer.infer_types;
renamed Type_Infer.polymorphicT to Type.mark_polymorphic;

--- a/src/Pure/Isar/proof_context.ML	Sun Sep 12 19:55:45 2010 +0200
+++ b/src/Pure/Isar/proof_context.ML	Sun Sep 12 20:47:47 2010 +0200
@@ -699,9 +699,7 @@
   in Variable.def_type ctxt pattern end;
 
 fun standard_infer_types ctxt ts =
-  Type_Infer.infer_types (Syntax.pp ctxt) (tsig_of ctxt) (Syntax.check_typs ctxt)
-    (try (Consts.the_constraint (consts_of ctxt))) (def_type ctxt)
-    (Variable.names_of ctxt) (Variable.maxidx_of ctxt) ts
+  Type_Infer.infer_types ctxt (try (Consts.the_constraint (consts_of ctxt))) (def_type ctxt) ts
   handle TYPE (msg, _, _) => error msg;
 
 local

--- a/src/Pure/ROOT.ML	Sun Sep 12 19:55:45 2010 +0200
+++ b/src/Pure/ROOT.ML	Sun Sep 12 20:47:47 2010 +0200
@@ -116,8 +116,6 @@
 use "Syntax/printer.ML";
 use "Syntax/syntax.ML";
 
-use "type_infer.ML";
-
 
 (* core of tactical proof system *)
 
@@ -159,6 +157,7 @@
 use "Isar/rule_cases.ML";
 use "Isar/auto_bind.ML";
 use "Isar/local_syntax.ML";
+use "type_infer.ML";
 use "Isar/proof_context.ML";
 use "Isar/local_defs.ML";
 

--- a/src/Pure/sign.ML	Sun Sep 12 19:55:45 2010 +0200
+++ b/src/Pure/sign.ML	Sun Sep 12 20:47:47 2010 +0200
@@ -29,6 +29,7 @@
   val defaultS: theory -> sort
   val subsort: theory -> sort * sort -> bool
   val of_sort: theory -> typ * sort -> bool
+  val inter_sort: theory -> sort * sort -> sort
   val witness_sorts: theory -> (typ * sort) list -> sort list -> (typ * sort) list
   val is_logtype: theory -> string -> bool
   val typ_instance: theory -> typ * typ -> bool
@@ -201,6 +202,7 @@
 val defaultS = Type.defaultS o tsig_of;
 val subsort = Type.subsort o tsig_of;
 val of_sort = Type.of_sort o tsig_of;
+val inter_sort = Type.inter_sort o tsig_of;
 val witness_sorts = Type.witness_sorts o tsig_of;
 val is_logtype = member (op =) o Type.logical_types o tsig_of;
 

--- a/src/Pure/type.ML	Sun Sep 12 19:55:45 2010 +0200
+++ b/src/Pure/type.ML	Sun Sep 12 20:47:47 2010 +0200
@@ -8,6 +8,7 @@
 signature TYPE =
 sig
   (*constraints*)
+  val mark_polymorphic: typ -> typ
   val constraint: typ -> term -> term
   val appl_error: Pretty.pp -> term -> typ -> term -> typ -> string
   (*type signatures and certified types*)
@@ -101,6 +102,9 @@
 
 (** constraints **)
 
+(*indicate polymorphic Vars*)
+fun mark_polymorphic T = Type ("_polymorphic_", [T]);
+
 fun constraint T t =
   if T = dummyT then t
   else Const ("_type_constraint_", T --> T) $ t;

--- a/src/Pure/type_infer.ML	Sun Sep 12 19:55:45 2010 +0200
+++ b/src/Pure/type_infer.ML	Sun Sep 12 20:47:47 2010 +0200
@@ -7,14 +7,12 @@
 signature TYPE_INFER =
 sig
   val anyT: sort -> typ
-  val polymorphicT: typ -> typ
   val is_param: indexname -> bool
   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 infer_types: Pretty.pp -> Type.tsig -> (typ list -> typ list) ->
-    (string -> typ option) -> (indexname -> typ option) -> Name.context -> int ->
+  val infer_types: Proof.context -> (string -> typ option) -> (indexname -> typ option) ->
     term list -> term list
 end;
 
@@ -26,9 +24,6 @@
 
 fun anyT S = TFree ("'_dummy_", S);
 
-(*indicate polymorphic Vars*)
-fun polymorphicT T = Type ("_polymorphic_", [T]);
-
 
 (* type inference parameters -- may get instantiated *)
 
@@ -235,12 +230,14 @@
 
 (* typs_terms_of *)
 
-fun typs_terms_of tye used maxidx (Ts, ts) =
+fun typs_terms_of ctxt tye (Ts, ts) =
   let
-    val used' = fold (add_names tye) ts (fold (add_namesT tye) Ts used);
+    val used = fold (add_names tye) ts (fold (add_namesT tye) Ts (Variable.names_of ctxt));
     val parms = rev (fold (add_parms tye) ts (fold (add_parmsT tye) Ts []));
-    val names = Name.invents used' ("?" ^ Name.aT) (length parms);
+    val names = Name.invents used ("?" ^ Name.aT) (length parms);
     val tab = Inttab.make (parms ~~ names);
+
+    val maxidx = Variable.maxidx_of ctxt;
     fun f i = (the (Inttab.lookup tab i), maxidx + 1);
   in (map (simple_typ_of tye f) Ts, map (simple_term_of tye f) ts) end;
 
@@ -250,27 +247,31 @@
 
 exception NO_UNIFIER of string * pretyp Inttab.table;
 
-fun unify pp tsig =
+fun unify ctxt pp =
   let
+    val thy = ProofContext.theory_of ctxt;
+    val arity_sorts = Type.arity_sorts pp (Sign.tsig_of thy);
+
+
     (* adjust sorts of parameters *)
 
     fun not_of_sort x S' S =
-      "Variable " ^ x ^ "::" ^ Pretty.string_of_sort pp S' ^ " not of sort " ^
-        Pretty.string_of_sort pp S;
+      "Variable " ^ x ^ "::" ^ Syntax.string_of_sort ctxt S' ^ " not of sort " ^
+        Syntax.string_of_sort ctxt S;
 
     fun meet (_, []) tye_idx = tye_idx
       | meet (Param (i, S'), S) (tye_idx as (tye, idx)) =
-          if Type.subsort tsig (S', S) then tye_idx
+          if Sign.subsort thy (S', S) then tye_idx
           else (Inttab.update_new (i,
-            Param (idx, Type.inter_sort tsig (S', S))) tye, idx + 1)
+            Param (idx, Sign.inter_sort thy (S', S))) tye, idx + 1)
       | meet (PType (a, Ts), S) (tye_idx as (tye, _)) =
-          meets (Ts, Type.arity_sorts pp tsig a S
+          meets (Ts, arity_sorts a S
             handle ERROR msg => raise NO_UNIFIER (msg, tye)) tye_idx
       | meet (PTFree (x, S'), S) (tye_idx as (tye, _)) =
-          if Type.subsort tsig (S', S) then tye_idx
+          if Sign.subsort thy (S', S) then tye_idx
           else raise NO_UNIFIER (not_of_sort x S' S, tye)
       | meet (PTVar (xi, S'), S) (tye_idx as (tye, _)) =
-          if Type.subsort tsig (S', S) then tye_idx
+          if Sign.subsort thy (S', S) then tye_idx
           else raise NO_UNIFIER (not_of_sort (Term.string_of_vname xi) S' S, tye)
     and meets (T :: Ts, S :: Ss) (tye_idx as (tye, _)) =
           meets (Ts, Ss) (meet (deref tye T, S) tye_idx)
@@ -298,7 +299,7 @@
     (* unification *)
 
     fun show_tycon (a, Ts) =
-      quote (Pretty.string_of_typ pp (Type (a, replicate (length Ts) dummyT)));
+      quote (Syntax.string_of_typ ctxt (Type (a, replicate (length Ts) dummyT)));
 
     fun unif (T1, T2) (tye_idx as (tye, idx)) =
       (case (deref tye T1, deref tye T2) of
@@ -319,13 +320,16 @@
 
 (* infer *)
 
-fun infer pp tsig =
+fun infer ctxt =
   let
+    val pp = Syntax.pp ctxt;
+
+
     (* errors *)
 
     fun prep_output tye bs ts Ts =
       let
-        val (Ts_bTs', ts') = typs_terms_of tye Name.context ~1 (Ts @ map snd bs, ts);
+        val (Ts_bTs', ts') = typs_terms_of ctxt tye (Ts @ map snd bs, ts);
         val (Ts', Ts'') = chop (length Ts) Ts_bTs';
         fun prep t =
           let val xs = rev (Term.variant_frees t (rev (map fst bs ~~ Ts'')))
@@ -355,8 +359,6 @@
 
     (* main *)
 
-    val unif = unify pp tsig;
-
     fun inf _ (PConst (_, T)) tye_idx = (T, tye_idx)
       | inf _ (PFree (_, T)) tye_idx = (T, tye_idx)
       | inf _ (PVar (_, T)) tye_idx = (T, tye_idx)
@@ -371,13 +373,13 @@
             val (U, (tye, idx)) = inf bs u tye_idx';
             val V = Param (idx, []);
             val U_to_V = PType ("fun", [U, V]);
-            val tye_idx'' = unif (U_to_V, T) (tye, idx + 1)
+            val tye_idx'' = unify ctxt pp (U_to_V, T) (tye, idx + 1)
               handle NO_UNIFIER (msg, tye') => err_appl msg tye' bs t T u U;
           in (V, tye_idx'') end
       | inf bs (Constraint (t, U)) tye_idx =
           let val (T, tye_idx') = inf bs t tye_idx in
             (T,
-             unif (T, U) tye_idx'
+             unify ctxt pp (T, U) tye_idx'
                handle NO_UNIFIER (msg, tye) => err_constraint msg tye bs t T U)
           end;
 
@@ -386,7 +388,7 @@
 
 (* infer_types *)
 
-fun infer_types pp tsig check_typs const_type var_type used maxidx raw_ts =
+fun infer_types ctxt const_type var_type raw_ts =
   let
     (*constrain vars*)
     val get_type = the_default dummyT o var_type;
@@ -396,13 +398,13 @@
         | t => t);
 
     (*convert to preterms*)
-    val ts = burrow_types check_typs raw_ts;
+    val ts = burrow_types (Syntax.check_typs ctxt) raw_ts;
     val (ts', (_, _, idx)) =
       fold_map (preterm_of const_type o constrain_vars) ts
       (Vartab.empty, Vartab.empty, 0);
 
     (*do type inference*)
-    val (tye, _) = fold (snd oo infer pp tsig) ts' (Inttab.empty, idx);
-  in #2 (typs_terms_of tye used maxidx ([], ts')) end;
+    val (tye, _) = fold (snd oo infer ctxt) ts' (Inttab.empty, idx);
+  in #2 (typs_terms_of ctxt tye ([], ts')) end;
 
 end;

--- a/src/Pure/variable.ML	Sun Sep 12 19:55:45 2010 +0200
+++ b/src/Pure/variable.ML	Sun Sep 12 20:47:47 2010 +0200
@@ -168,7 +168,7 @@
     (case Vartab.lookup types xi of
       NONE =>
         if pattern then NONE
-        else Vartab.lookup binds xi |> Option.map (Type_Infer.polymorphicT o #1)
+        else Vartab.lookup binds xi |> Option.map (Type.mark_polymorphic o #1)
     | some => some)
   end;
 

--- a/src/Tools/nbe.ML	Sun Sep 12 19:55:45 2010 +0200
+++ b/src/Tools/nbe.ML	Sun Sep 12 20:47:47 2010 +0200
@@ -547,13 +547,13 @@
 
 fun normalize thy program ((vs0, (vs, ty)), t) deps =
   let
+    val ctxt = Syntax.init_pretty_global thy;
     val ty' = typ_of_itype program vs0 ty;
     fun type_infer t =
-      singleton (Type_Infer.infer_types (Syntax.pp_global thy) (Sign.tsig_of thy) I
-        (try (Type.strip_sorts o Sign.the_const_type thy)) (K NONE) Name.context 0)
-      (Type.constraint ty' t);
-    val string_of_term =
-      Syntax.string_of_term (Config.put show_types true (Syntax.init_pretty_global thy));
+      singleton
+        (Type_Infer.infer_types ctxt (try (Type.strip_sorts o Sign.the_const_type thy)) (K NONE))
+        (Type.constraint ty' t);
+    val string_of_term = Syntax.string_of_term (Config.put show_types true ctxt);
     fun check_tvars t =
       if null (Term.add_tvars t []) then t
       else error ("Illegal schematic type variables in normalized term: " ^ string_of_term t);