renamed structure TypeInfer to Type_Infer, keeping the old name as legacy alias for some time;
authorwenzelm
Thu May 27 17:41:27 2010 +0200 (2010-05-27)
changeset 3714501aa36932739
parent 37144 fd6308b4df72
child 37146 f652333bbf8e
renamed structure TypeInfer to Type_Infer, keeping the old name as legacy alias for some time;
NEWS
src/HOL/Import/proof_kernel.ML
src/HOL/Tools/Function/function.ML
src/HOL/Tools/Function/function_core.ML
src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML
src/HOL/Tools/hologic.ML
src/HOL/Tools/primrec.ML
src/HOLCF/Tools/Domain/domain_library.ML
src/HOLCF/Tools/Domain/domain_theorems.ML
src/Pure/Isar/class_target.ML
src/Pure/Isar/expression.ML
src/Pure/Isar/proof_context.ML
src/Pure/Isar/rule_insts.ML
src/Pure/Isar/specification.ML
src/Pure/Proof/proof_syntax.ML
src/Pure/ROOT.ML
src/Pure/Thy/thy_output.ML
src/Pure/old_goals.ML
src/Pure/sign.ML
src/Pure/type_infer.ML
src/Pure/variable.ML
src/Tools/nbe.ML
src/ZF/Tools/datatype_package.ML
src/ZF/Tools/inductive_package.ML
src/ZF/ind_syntax.ML
     1.1 --- a/NEWS	Thu May 27 15:28:23 2010 +0200
     1.2 +++ b/NEWS	Thu May 27 17:41:27 2010 +0200
     1.3 @@ -502,6 +502,7 @@
     1.4    OuterParse    ~>  Parse
     1.5    OuterSyntax   ~>  Outer_Syntax
     1.6    SpecParse     ~>  Parse_Spec
     1.7 +  TypeInfer     ~>  Type_Infer
     1.8  
     1.9  Note that "open Legacy" simplifies porting of sources, but forgetting
    1.10  to remove it again will complicate porting again in the future.
     2.1 --- a/src/HOL/Import/proof_kernel.ML	Thu May 27 15:28:23 2010 +0200
     2.2 +++ b/src/HOL/Import/proof_kernel.ML	Thu May 27 17:41:27 2010 +0200
     2.3 @@ -229,7 +229,7 @@
     2.4                  val str =
     2.5                    setmp_CRITICAL show_brackets false (G n (Syntax.string_of_term ctxt o term_of)) ct
     2.6                  val u = Syntax.parse_term ctxt str
     2.7 -                  |> TypeInfer.constrain T |> Syntax.check_term ctxt
     2.8 +                  |> Type_Infer.constrain T |> Syntax.check_term ctxt
     2.9              in
    2.10                  if match u
    2.11                  then quote str
     3.1 --- a/src/HOL/Tools/Function/function.ML	Thu May 27 15:28:23 2010 +0200
     3.2 +++ b/src/HOL/Tools/Function/function.ML	Thu May 27 17:41:27 2010 +0200
     3.3 @@ -149,7 +149,7 @@
     3.4    end
     3.5  
     3.6  val add_function =
     3.7 -  gen_add_function false Specification.check_spec (TypeInfer.anyT HOLogic.typeS)
     3.8 +  gen_add_function false Specification.check_spec (Type_Infer.anyT HOLogic.typeS)
     3.9  val add_function_cmd = gen_add_function true Specification.read_spec "_::type"
    3.10  
    3.11  fun gen_function is_external prep default_constraint fixspec eqns config lthy =
    3.12 @@ -163,7 +163,7 @@
    3.13    end
    3.14  
    3.15  val function =
    3.16 -  gen_function false Specification.check_spec (TypeInfer.anyT HOLogic.typeS)
    3.17 +  gen_function false Specification.check_spec (Type_Infer.anyT HOLogic.typeS)
    3.18  val function_cmd = gen_function true Specification.read_spec "_::type"
    3.19  
    3.20  fun prepare_termination_proof prep_term raw_term_opt lthy =
     4.1 --- a/src/HOL/Tools/Function/function_core.ML	Thu May 27 15:28:23 2010 +0200
     4.2 +++ b/src/HOL/Tools/Function/function_core.ML	Thu May 27 17:41:27 2010 +0200
     4.3 @@ -879,7 +879,7 @@
     4.4      val ranT = range_type fT
     4.5  
     4.6      val default = Syntax.parse_term lthy default_str
     4.7 -      |> TypeInfer.constrain fT |> Syntax.check_term lthy
     4.8 +      |> Type_Infer.constrain fT |> Syntax.check_term lthy
     4.9  
    4.10      val (globals, ctxt') = fix_globals domT ranT fvar lthy
    4.11  
     5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Thu May 27 15:28:23 2010 +0200
     5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Thu May 27 17:41:27 2010 +0200
     5.3 @@ -254,7 +254,7 @@
     5.4              SOME b => TVar (("'" ^ b, 0), HOLogic.typeS)
     5.5            | NONE =>
     5.6              (* Variable from the ATP, say "X1" *)
     5.7 -            TypeInfer.param 0 (a, HOLogic.typeS)
     5.8 +            Type_Infer.param 0 (a, HOLogic.typeS)
     5.9      end
    5.10  
    5.11  (*Invert the table of translations between Isabelle and ATPs*)
    5.12 @@ -453,7 +453,7 @@
    5.13      val (vt, t) = lits_of_nodes thy full_types tfrees (Vartab.empty, []) us
    5.14    in repair_tvar_sorts vt t end
    5.15  fun check_formula ctxt =
    5.16 -  TypeInfer.constrain @{typ bool}
    5.17 +  Type_Infer.constrain @{typ bool}
    5.18    #> Syntax.check_term (ProofContext.set_mode ProofContext.mode_schematic ctxt)
    5.19  
    5.20  
     6.1 --- a/src/HOL/Tools/hologic.ML	Thu May 27 15:28:23 2010 +0200
     6.2 +++ b/src/HOL/Tools/hologic.ML	Thu May 27 17:41:27 2010 +0200
     6.3 @@ -138,7 +138,7 @@
     6.4  (* HOL syntax *)
     6.5  
     6.6  val typeS: sort = ["HOL.type"];
     6.7 -val typeT = TypeInfer.anyT typeS;
     6.8 +val typeT = Type_Infer.anyT typeS;
     6.9  
    6.10  
    6.11  (* bool and set *)
     7.1 --- a/src/HOL/Tools/primrec.ML	Thu May 27 15:28:23 2010 +0200
     7.2 +++ b/src/HOL/Tools/primrec.ML	Thu May 27 17:41:27 2010 +0200
     7.3 @@ -197,7 +197,7 @@
     7.4      val raw_rhs = fold_rev (fn T => fn t => Abs ("", T, t)) (map snd ls @ [dummyT])
     7.5        (list_comb (Const (rec_name, dummyT), fs @ map Bound (0 :: (length ls downto 1))))
     7.6      val rhs = singleton (Syntax.check_terms ctxt)
     7.7 -      (TypeInfer.constrain varT raw_rhs);
     7.8 +      (Type_Infer.constrain varT raw_rhs);
     7.9    in (var, ((Binding.conceal (Binding.name def_name), []), rhs)) end;
    7.10  
    7.11  
     8.1 --- a/src/HOLCF/Tools/Domain/domain_library.ML	Thu May 27 15:28:23 2010 +0200
     8.2 +++ b/src/HOLCF/Tools/Domain/domain_library.ML	Thu May 27 17:41:27 2010 +0200
     8.3 @@ -185,7 +185,7 @@
     8.4  fun mk_lam  (x,T) = Abs(x,dummyT,T);
     8.5  fun mk_all  (x,P) = HOLogic.mk_all (x,dummyT,P);
     8.6  fun mk_ex   (x,P) = mk_exists (x,dummyT,P);
     8.7 -fun mk_constrainall (x,typ,P) = %%:"All" $ (TypeInfer.constrain (typ --> boolT) (mk_lam(x,P)));
     8.8 +fun mk_constrainall (x,typ,P) = %%:"All" $ (Type_Infer.constrain (typ --> boolT) (mk_lam(x,P)));
     8.9  end
    8.10  
    8.11  fun mk_All  (x,P) = %%:"all" $ mk_lam(x,P); (* meta universal quantification *)
     9.1 --- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Thu May 27 15:28:23 2010 +0200
     9.2 +++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Thu May 27 17:41:27 2010 +0200
     9.3 @@ -463,7 +463,7 @@
     9.4  
     9.5    fun legacy_infer_term thy t =
     9.6        singleton (Syntax.check_terms (ProofContext.init_global thy)) (intern_term thy t);
     9.7 -  fun legacy_infer_prop thy t = legacy_infer_term thy (TypeInfer.constrain propT t);
     9.8 +  fun legacy_infer_prop thy t = legacy_infer_term thy (Type_Infer.constrain propT t);
     9.9    fun infer_props thy = map (apsnd (legacy_infer_prop thy));
    9.10    fun add_defs_i x = PureThy.add_defs false (map Thm.no_attributes x);
    9.11    fun add_defs_infer defs thy = add_defs_i (infer_props thy defs) thy;
    10.1 --- a/src/Pure/Isar/class_target.ML	Thu May 27 15:28:23 2010 +0200
    10.2 +++ b/src/Pure/Isar/class_target.ML	Thu May 27 17:41:27 2010 +0200
    10.3 @@ -275,7 +275,7 @@
    10.4       of SOME ty' => (case try (Type.raw_match (ty', ty)) Vartab.empty
    10.5           of SOME tyenv => (case Vartab.lookup tyenv (Name.aT, 0)
    10.6               of SOME (_, ty' as TVar (vi, sort)) =>
    10.7 -                  if TypeInfer.is_param vi
    10.8 +                  if Type_Infer.is_param vi
    10.9                      andalso Sorts.sort_le algebra (base_sort, sort)
   10.10                        then SOME (ty', TFree (Name.aT, base_sort))
   10.11                        else NONE
    11.1 --- a/src/Pure/Isar/expression.ML	Thu May 27 15:28:23 2010 +0200
    11.2 +++ b/src/Pure/Isar/expression.ML	Thu May 27 17:41:27 2010 +0200
    11.3 @@ -162,9 +162,9 @@
    11.4      val type_parm_names = fold Term.add_tfreesT parm_types [] |> map fst;
    11.5  
    11.6      (* type inference and contexts *)
    11.7 -    val parm_types' = map (TypeInfer.paramify_vars o Logic.varifyT_global) parm_types;
    11.8 +    val parm_types' = map (Type_Infer.paramify_vars o Logic.varifyT_global) parm_types;
    11.9      val type_parms = fold Term.add_tvarsT parm_types' [] |> map (Logic.mk_type o TVar);
   11.10 -    val arg = type_parms @ map2 TypeInfer.constrain parm_types' insts';
   11.11 +    val arg = type_parms @ map2 Type_Infer.constrain parm_types' insts';
   11.12      val res = Syntax.check_terms ctxt arg;
   11.13      val ctxt' = ctxt |> fold Variable.auto_fixes res;
   11.14  
   11.15 @@ -345,9 +345,9 @@
   11.16        let
   11.17          val (parm_names, parm_types) = Locale.params_of thy loc |> map #1 |> split_list;
   11.18          val inst' = prep_inst ctxt parm_names inst;
   11.19 -        val parm_types' = map (TypeInfer.paramify_vars o
   11.20 +        val parm_types' = map (Type_Infer.paramify_vars o
   11.21            Term.map_type_tvar (fn ((x, _), S) => TVar ((x, i), S)) o Logic.varifyT_global) parm_types;
   11.22 -        val inst'' = map2 TypeInfer.constrain parm_types' inst';
   11.23 +        val inst'' = map2 Type_Infer.constrain parm_types' inst';
   11.24          val insts' = insts @ [(loc, (prfx, inst''))];
   11.25          val (insts'', _, _, ctxt' (* FIXME not used *) ) = check_autofix insts' [] [] ctxt;
   11.26          val inst''' = insts'' |> List.last |> snd |> snd;
    12.1 --- a/src/Pure/Isar/proof_context.ML	Thu May 27 15:28:23 2010 +0200
    12.2 +++ b/src/Pure/Isar/proof_context.ML	Thu May 27 17:41:27 2010 +0200
    12.3 @@ -577,7 +577,7 @@
    12.4        pattern orelse schematic orelse
    12.5          T |> Term.exists_subtype
    12.6            (fn TVar (xi, _) =>
    12.7 -            not (TypeInfer.is_param xi) andalso
    12.8 +            not (Type_Infer.is_param xi) andalso
    12.9                error ("Illegal schematic type variable: " ^ Term.string_of_vname xi)
   12.10            | _ => false)
   12.11    in T end;
   12.12 @@ -599,7 +599,7 @@
   12.13  
   12.14  fun prepare_patterns ctxt =
   12.15    let val Mode {pattern, ...} = get_mode ctxt in
   12.16 -    TypeInfer.fixate_params (Variable.names_of ctxt) #>
   12.17 +    Type_Infer.fixate_params (Variable.names_of ctxt) #>
   12.18      pattern ? Variable.polymorphic ctxt #>
   12.19      (map o Term.map_types) (prepare_patternT ctxt) #>
   12.20      (if pattern then prepare_dummies else map (check_dummies ctxt))
   12.21 @@ -699,7 +699,7 @@
   12.22    in Variable.def_type ctxt pattern end;
   12.23  
   12.24  fun standard_infer_types ctxt ts =
   12.25 -  TypeInfer.infer_types (Syntax.pp ctxt) (tsig_of ctxt) (Syntax.check_typs ctxt)
   12.26 +  Type_Infer.infer_types (Syntax.pp ctxt) (tsig_of ctxt) (Syntax.check_typs ctxt)
   12.27      (try (Consts.the_constraint (consts_of ctxt))) (def_type ctxt)
   12.28      (Variable.names_of ctxt) (Variable.maxidx_of ctxt) ts
   12.29    handle TYPE (msg, _, _) => error msg;
   12.30 @@ -754,11 +754,11 @@
   12.31    let
   12.32      val {get_sort, map_const, map_free} = term_context ctxt;
   12.33  
   12.34 -    val (T', _) = TypeInfer.paramify_dummies T 0;
   12.35 +    val (T', _) = Type_Infer.paramify_dummies T 0;
   12.36      val (markup, kind) = if T' = propT then (Markup.prop, "proposition") else (Markup.term, "term");
   12.37      val (syms, pos) = Syntax.parse_token markup text;
   12.38  
   12.39 -    fun check t = (Syntax.check_term ctxt (TypeInfer.constrain T' t); NONE)
   12.40 +    fun check t = (Syntax.check_term ctxt (Type_Infer.constrain T' t); NONE)
   12.41        handle ERROR msg => SOME msg;
   12.42      val t =
   12.43        Syntax.standard_parse_term (Syntax.pp ctxt) check get_sort map_const map_free
   12.44 @@ -883,7 +883,7 @@
   12.45  in
   12.46  
   12.47  fun read_terms ctxt T =
   12.48 -  map (Syntax.parse_term ctxt #> TypeInfer.constrain T) #> Syntax.check_terms ctxt;
   12.49 +  map (Syntax.parse_term ctxt #> Type_Infer.constrain T) #> Syntax.check_terms ctxt;
   12.50  
   12.51  val match_bind = gen_bind read_terms;
   12.52  val match_bind_i = gen_bind (fn ctxt => fn _ => map (cert_term ctxt));
    13.1 --- a/src/Pure/Isar/rule_insts.ML	Thu May 27 15:28:23 2010 +0200
    13.2 +++ b/src/Pure/Isar/rule_insts.ML	Thu May 27 17:41:27 2010 +0200
    13.3 @@ -82,7 +82,7 @@
    13.4      fun parse T = if T = propT then Syntax.parse_prop ctxt else Syntax.parse_term ctxt;
    13.5      val ts = map2 parse Ts ss;
    13.6      val ts' =
    13.7 -      map2 (TypeInfer.constrain o TypeInfer.paramify_vars) Ts ts
    13.8 +      map2 (Type_Infer.constrain o Type_Infer.paramify_vars) Ts ts
    13.9        |> Syntax.check_terms ((schematic ? ProofContext.set_mode ProofContext.mode_schematic) ctxt)
   13.10        |> Variable.polymorphic ctxt;
   13.11      val Ts' = map Term.fastype_of ts';
    14.1 --- a/src/Pure/Isar/specification.ML	Thu May 27 15:28:23 2010 +0200
    14.2 +++ b/src/Pure/Isar/specification.ML	Thu May 27 17:41:27 2010 +0200
    14.3 @@ -96,13 +96,13 @@
    14.4        (case duplicates (op =) commons of [] => ()
    14.5        | dups => error ("Duplicate local variables " ^ commas_quote dups));
    14.6      val frees = rev ((fold o fold_aterms) add_free As (rev commons));
    14.7 -    val types = map (TypeInfer.param i o rpair []) (Name.invents Name.context Name.aT (length frees));
    14.8 +    val types = map (Type_Infer.param i o rpair []) (Name.invents Name.context Name.aT (length frees));
    14.9      val uniform_typing = the o AList.lookup (op =) (frees ~~ types);
   14.10  
   14.11      fun abs_body lev y (Abs (x, T, b)) = Abs (x, T, abs_body (lev + 1) y b)
   14.12        | abs_body lev y (t $ u) = abs_body lev y t $ abs_body lev y u
   14.13        | abs_body lev y (t as Free (x, T)) =
   14.14 -          if x = y then TypeInfer.constrain (uniform_typing x) (TypeInfer.constrain T (Bound lev))
   14.15 +          if x = y then Type_Infer.constrain (uniform_typing x) (Type_Infer.constrain T (Bound lev))
   14.16            else t
   14.17        | abs_body _ _ a = a;
   14.18      fun close (y, U) B =
    15.1 --- a/src/Pure/Proof/proof_syntax.ML	Thu May 27 15:28:23 2010 +0200
    15.2 +++ b/src/Pure/Proof/proof_syntax.ML	Thu May 27 17:41:27 2010 +0200
    15.3 @@ -212,7 +212,7 @@
    15.4    in
    15.5      fn ty => fn s =>
    15.6        (if ty = propT then Syntax.parse_prop else Syntax.parse_term) ctxt s
    15.7 -      |> TypeInfer.constrain ty |> Syntax.check_term ctxt
    15.8 +      |> Type_Infer.constrain ty |> Syntax.check_term ctxt
    15.9    end;
   15.10  
   15.11  fun read_proof thy =
    16.1 --- a/src/Pure/ROOT.ML	Thu May 27 15:28:23 2010 +0200
    16.2 +++ b/src/Pure/ROOT.ML	Thu May 27 17:41:27 2010 +0200
    16.3 @@ -309,6 +309,7 @@
    16.4  structure OuterParse = Parse;
    16.5  structure OuterSyntax = Outer_Syntax;
    16.6  structure SpecParse = Parse_Spec;
    16.7 +structure TypeInfer = Type_Infer;
    16.8  
    16.9  end;
   16.10  
    17.1 --- a/src/Pure/Thy/thy_output.ML	Thu May 27 15:28:23 2010 +0200
    17.2 +++ b/src/Pure/Thy/thy_output.ML	Thu May 27 17:41:27 2010 +0200
    17.3 @@ -455,7 +455,7 @@
    17.4  
    17.5  fun pretty_term_typ ctxt (style, t) =
    17.6    let val t' = style t
    17.7 -  in pretty_term ctxt (TypeInfer.constrain (Term.fastype_of t') t') end;
    17.8 +  in pretty_term ctxt (Type_Infer.constrain (Term.fastype_of t') t') end;
    17.9  
   17.10  fun pretty_term_typeof ctxt (style, t) =
   17.11    Syntax.pretty_typ ctxt (Term.fastype_of (style t));
    18.1 --- a/src/Pure/old_goals.ML	Thu May 27 15:28:23 2010 +0200
    18.2 +++ b/src/Pure/old_goals.ML	Thu May 27 17:41:27 2010 +0200
    18.3 @@ -223,7 +223,7 @@
    18.4        |> ProofContext.allow_dummies
    18.5        |> ProofContext.set_mode ProofContext.mode_schematic;
    18.6      val parse = if T = propT then Syntax.parse_prop else Syntax.parse_term;
    18.7 -  in parse ctxt s |> TypeInfer.constrain T |> Syntax.check_term ctxt end;
    18.8 +  in parse ctxt s |> Type_Infer.constrain T |> Syntax.check_term ctxt end;
    18.9  
   18.10  fun read_term thy = simple_read_term thy dummyT;
   18.11  fun read_prop thy = simple_read_term thy propT;
    19.1 --- a/src/Pure/sign.ML	Thu May 27 15:28:23 2010 +0200
    19.2 +++ b/src/Pure/sign.ML	Thu May 27 17:41:27 2010 +0200
    19.3 @@ -271,7 +271,7 @@
    19.4          val t' = subst_bounds (xs, t);
    19.5          val u' = subst_bounds (xs, u);
    19.6          val msg = cat_lines
    19.7 -          (TypeInfer.appl_error (Syntax.pp_show_brackets pp) why t' T u' U);
    19.8 +          (Type_Infer.appl_error (Syntax.pp_show_brackets pp) why t' T u' U);
    19.9        in raise TYPE (msg, [T, U], [t', u']) end;
   19.10  
   19.11      fun typ_of (_, Const (_, T)) = T
    20.1 --- a/src/Pure/type_infer.ML	Thu May 27 15:28:23 2010 +0200
    20.2 +++ b/src/Pure/type_infer.ML	Thu May 27 17:41:27 2010 +0200
    20.3 @@ -20,7 +20,7 @@
    20.4      term list -> term list
    20.5  end;
    20.6  
    20.7 -structure TypeInfer: TYPE_INFER =
    20.8 +structure Type_Infer: TYPE_INFER =
    20.9  struct
   20.10  
   20.11  
    21.1 --- a/src/Pure/variable.ML	Thu May 27 15:28:23 2010 +0200
    21.2 +++ b/src/Pure/variable.ML	Thu May 27 17:41:27 2010 +0200
    21.3 @@ -168,7 +168,7 @@
    21.4      (case Vartab.lookup types xi of
    21.5        NONE =>
    21.6          if pattern then NONE
    21.7 -        else Vartab.lookup binds xi |> Option.map (TypeInfer.polymorphicT o #1)
    21.8 +        else Vartab.lookup binds xi |> Option.map (Type_Infer.polymorphicT o #1)
    21.9      | some => some)
   21.10    end;
   21.11  
    22.1 --- a/src/Tools/nbe.ML	Thu May 27 15:28:23 2010 +0200
    22.2 +++ b/src/Tools/nbe.ML	Thu May 27 17:41:27 2010 +0200
    22.3 @@ -506,7 +506,7 @@
    22.4              val ts' = take_until is_dict ts;
    22.5              val c = const_of_idx idx;
    22.6              val T = map_type_tvar (fn ((v, i), _) =>
    22.7 -              TypeInfer.param typidx (v ^ string_of_int i, []))
    22.8 +              Type_Infer.param typidx (v ^ string_of_int i, []))
    22.9                  (Sign.the_const_type thy c);
   22.10              val typidx' = typidx + 1;
   22.11            in of_apps bounds (Term.Const (c, T), ts') typidx' end
   22.12 @@ -548,9 +548,9 @@
   22.13    let
   22.14      val ty' = typ_of_itype program vs0 ty;
   22.15      fun type_infer t =
   22.16 -      singleton (TypeInfer.infer_types (Syntax.pp_global thy) (Sign.tsig_of thy) I
   22.17 +      singleton (Type_Infer.infer_types (Syntax.pp_global thy) (Sign.tsig_of thy) I
   22.18          (try (Type.strip_sorts o Sign.the_const_type thy)) (K NONE) Name.context 0)
   22.19 -      (TypeInfer.constrain ty' t);
   22.20 +      (Type_Infer.constrain ty' t);
   22.21      fun check_tvars t = if null (Term.add_tvars t []) then t else
   22.22        error ("Illegal schematic type variables in normalized term: "
   22.23          ^ setmp_CRITICAL show_types true (Syntax.string_of_term_global thy) t);
    23.1 --- a/src/ZF/Tools/datatype_package.ML	Thu May 27 15:28:23 2010 +0200
    23.2 +++ b/src/ZF/Tools/datatype_package.ML	Thu May 27 17:41:27 2010 +0200
    23.3 @@ -403,7 +403,7 @@
    23.4    let
    23.5      val ctxt = ProofContext.init_global thy;
    23.6      fun read_is strs =
    23.7 -      map (Syntax.parse_term ctxt #> TypeInfer.constrain @{typ i}) strs
    23.8 +      map (Syntax.parse_term ctxt #> Type_Infer.constrain @{typ i}) strs
    23.9        |> Syntax.check_terms ctxt;
   23.10  
   23.11      val rec_tms = read_is srec_tms;
    24.1 --- a/src/ZF/Tools/inductive_package.ML	Thu May 27 15:28:23 2010 +0200
    24.2 +++ b/src/ZF/Tools/inductive_package.ML	Thu May 27 17:41:27 2010 +0200
    24.3 @@ -555,7 +555,7 @@
    24.4      (raw_monos, raw_con_defs, raw_type_intrs, raw_type_elims) thy =
    24.5    let
    24.6      val ctxt = ProofContext.init_global thy;
    24.7 -    val read_terms = map (Syntax.parse_term ctxt #> TypeInfer.constrain Ind_Syntax.iT)
    24.8 +    val read_terms = map (Syntax.parse_term ctxt #> Type_Infer.constrain Ind_Syntax.iT)
    24.9        #> Syntax.check_terms ctxt;
   24.10  
   24.11      val intr_atts = map (map (Attrib.attribute thy) o snd) intr_srcs;
    25.1 --- a/src/ZF/ind_syntax.ML	Thu May 27 15:28:23 2010 +0200
    25.2 +++ b/src/ZF/ind_syntax.ML	Thu May 27 17:41:27 2010 +0200
    25.3 @@ -66,7 +66,7 @@
    25.4  
    25.5  (*read a constructor specification*)
    25.6  fun read_construct ctxt (id: string, sprems, syn: mixfix) =
    25.7 -    let val prems = map (Syntax.parse_term ctxt #> TypeInfer.constrain FOLogic.oT) sprems
    25.8 +    let val prems = map (Syntax.parse_term ctxt #> Type_Infer.constrain FOLogic.oT) sprems
    25.9            |> Syntax.check_terms ctxt
   25.10          val args = map (#1 o dest_mem) prems
   25.11          val T = (map (#2 o dest_Free) args) ---> iT