--- 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));