diff -r fd6308b4df72 -r 01aa36932739 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Thu May 27 15:28:23 2010 +0200
+++ b/src/Pure/Isar/proof_context.ML	Thu May 27 17:41:27 2010 +0200
@@ -577,7 +577,7 @@
       pattern orelse schematic orelse
         T |> Term.exists_subtype
           (fn TVar (xi, _) =>
-            not (TypeInfer.is_param xi) andalso
+            not (Type_Infer.is_param xi) andalso
               error ("Illegal schematic type variable: " ^ Term.string_of_vname xi)
           | _ => false)
   in T end;
@@ -599,7 +599,7 @@
 
 fun prepare_patterns ctxt =
   let val Mode {pattern, ...} = get_mode ctxt in
-    TypeInfer.fixate_params (Variable.names_of ctxt) #>
+    Type_Infer.fixate_params (Variable.names_of ctxt) #>
     pattern ? Variable.polymorphic ctxt #>
     (map o Term.map_types) (prepare_patternT ctxt) #>
     (if pattern then prepare_dummies else map (check_dummies ctxt))
@@ -699,7 +699,7 @@
   in Variable.def_type ctxt pattern end;
 
 fun standard_infer_types ctxt ts =
-  TypeInfer.infer_types (Syntax.pp ctxt) (tsig_of ctxt) (Syntax.check_typs ctxt)
+  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
   handle TYPE (msg, _, _) => error msg;
@@ -754,11 +754,11 @@
   let
     val {get_sort, map_const, map_free} = term_context ctxt;
 
-    val (T', _) = TypeInfer.paramify_dummies T 0;
+    val (T', _) = Type_Infer.paramify_dummies T 0;
     val (markup, kind) = if T' = propT then (Markup.prop, "proposition") else (Markup.term, "term");
     val (syms, pos) = Syntax.parse_token markup text;
 
-    fun check t = (Syntax.check_term ctxt (TypeInfer.constrain T' t); NONE)
+    fun check t = (Syntax.check_term ctxt (Type_Infer.constrain T' t); NONE)
       handle ERROR msg => SOME msg;
     val t =
       Syntax.standard_parse_term (Syntax.pp ctxt) check get_sort map_const map_free
@@ -883,7 +883,7 @@
 in
 
 fun read_terms ctxt T =
-  map (Syntax.parse_term ctxt #> TypeInfer.constrain T) #> Syntax.check_terms ctxt;
+  map (Syntax.parse_term ctxt #> Type_Infer.constrain T) #> Syntax.check_terms ctxt;
 
 val match_bind = gen_bind read_terms;
 val match_bind_i = gen_bind (fn ctxt => fn _ => map (cert_term ctxt));