1.1 --- a/src/Pure/Isar/proof_context.ML	Thu May 27 15:28:23 2010 +0200
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Thu May 27 17:41:27 2010 +0200
     1.3 @@ -577,7 +577,7 @@
     1.4        pattern orelse schematic orelse
     1.5          T |> Term.exists_subtype
     1.6            (fn TVar (xi, _) =>
     1.7 -            not (TypeInfer.is_param xi) andalso
     1.8 +            not (Type_Infer.is_param xi) andalso
     1.9                error ("Illegal schematic type variable: " ^ Term.string_of_vname xi)
    1.10            | _ => false)
    1.11    in T end;
    1.12 @@ -599,7 +599,7 @@
    1.13  
    1.14  fun prepare_patterns ctxt =
    1.15    let val Mode {pattern, ...} = get_mode ctxt in
    1.16 -    TypeInfer.fixate_params (Variable.names_of ctxt) #>
    1.17 +    Type_Infer.fixate_params (Variable.names_of ctxt) #>
    1.18      pattern ? Variable.polymorphic ctxt #>
    1.19      (map o Term.map_types) (prepare_patternT ctxt) #>
    1.20      (if pattern then prepare_dummies else map (check_dummies ctxt))
    1.21 @@ -699,7 +699,7 @@
    1.22    in Variable.def_type ctxt pattern end;
    1.23  
    1.24  fun standard_infer_types ctxt ts =
    1.25 -  TypeInfer.infer_types (Syntax.pp ctxt) (tsig_of ctxt) (Syntax.check_typs ctxt)
    1.26 +  Type_Infer.infer_types (Syntax.pp ctxt) (tsig_of ctxt) (Syntax.check_typs ctxt)
    1.27      (try (Consts.the_constraint (consts_of ctxt))) (def_type ctxt)
    1.28      (Variable.names_of ctxt) (Variable.maxidx_of ctxt) ts
    1.29    handle TYPE (msg, _, _) => error msg;
    1.30 @@ -754,11 +754,11 @@
    1.31    let
    1.32      val {get_sort, map_const, map_free} = term_context ctxt;
    1.33  
    1.34 -    val (T', _) = TypeInfer.paramify_dummies T 0;
    1.35 +    val (T', _) = Type_Infer.paramify_dummies T 0;
    1.36      val (markup, kind) = if T' = propT then (Markup.prop, "proposition") else (Markup.term, "term");
    1.37      val (syms, pos) = Syntax.parse_token markup text;
    1.38  
    1.39 -    fun check t = (Syntax.check_term ctxt (TypeInfer.constrain T' t); NONE)
    1.40 +    fun check t = (Syntax.check_term ctxt (Type_Infer.constrain T' t); NONE)
    1.41        handle ERROR msg => SOME msg;
    1.42      val t =
    1.43        Syntax.standard_parse_term (Syntax.pp ctxt) check get_sort map_const map_free
    1.44 @@ -883,7 +883,7 @@
    1.45  in
    1.46  
    1.47  fun read_terms ctxt T =
    1.48 -  map (Syntax.parse_term ctxt #> TypeInfer.constrain T) #> Syntax.check_terms ctxt;
    1.49 +  map (Syntax.parse_term ctxt #> Type_Infer.constrain T) #> Syntax.check_terms ctxt;
    1.50  
    1.51  val match_bind = gen_bind read_terms;
    1.52  val match_bind_i = gen_bind (fn ctxt => fn _ => map (cert_term ctxt));