--- a/src/HOL/Nominal/nominal_primrec.ML Thu Aug 30 21:44:29 2007 +0200
+++ b/src/HOL/Nominal/nominal_primrec.ML Thu Aug 30 22:35:34 2007 +0200
@@ -211,7 +211,7 @@
list_comb (Const (rec_name, dummyT), fs @ [Free x]))
val def_name = Sign.base_name fname ^ "_" ^ Sign.base_name tname ^ "_def";
val def_prop as _ $ _ $ t =
- singleton (ProofContext.infer_types (ProofContext.init thy))
+ singleton (Syntax.check_terms (ProofContext.init thy))
(Logic.mk_equals (Const (fname, dummyT), rhs));
in ((def_name, def_prop), subst_bounds (rev (map Free frees), strip_abs_body t)) end;
--- a/src/HOL/Tools/TFL/tfl.ML Thu Aug 30 21:44:29 2007 +0200
+++ b/src/HOL/Tools/TFL/tfl.ML Thu Aug 30 22:35:34 2007 +0200
@@ -367,7 +367,7 @@
(*For Isabelle, the lhs of a definition must be a constant.*)
fun mk_const_def sign (c, Ty, rhs) =
- singleton (ProofContext.infer_types (ProofContext.init sign))
+ singleton (Syntax.check_terms (ProofContext.init sign))
(Sign.intern_term sign (Const("==",dummyT) $ Const(c,Ty) $ rhs));
(*Make all TVars available for instantiation by adding a ? to the front*)
--- a/src/HOL/Tools/primrec_package.ML Thu Aug 30 21:44:29 2007 +0200
+++ b/src/HOL/Tools/primrec_package.ML Thu Aug 30 22:35:34 2007 +0200
@@ -227,7 +227,7 @@
fs @ map Bound (0 ::(length ls downto 1))))
val def_name = Sign.base_name fname ^ "_" ^ Sign.base_name tname ^ "_def";
val def_prop =
- singleton (ProofContext.infer_types (ProofContext.init thy))
+ singleton (Syntax.check_terms (ProofContext.init thy))
(Logic.mk_equals (Const (fname, dummyT), rhs));
in (def_name, def_prop) end;
--- a/src/HOL/Tools/res_reconstruct.ML Thu Aug 30 21:44:29 2007 +0200
+++ b/src/HOL/Tools/res_reconstruct.ML Thu Aug 30 22:35:34 2007 +0200
@@ -238,7 +238,7 @@
vt0 holds the initial sort constraints, from the conjecture clauses.*)
fun clause_of_strees ctxt vt0 ts =
let val (vt, dt) = lits_of_strees ctxt (vt0,[]) ts in
- singleton (ProofContext.infer_types ctxt) (TypeInfer.constrain (fix_sorts vt dt) HOLogic.boolT)
+ singleton (Syntax.check_terms ctxt) (TypeInfer.constrain (fix_sorts vt dt) HOLogic.boolT)
end;
(*Quantification over a list of Vars. FIXME: for term.ML??*)
--- a/src/HOLCF/Tools/fixrec_package.ML Thu Aug 30 21:44:29 2007 +0200
+++ b/src/HOLCF/Tools/fixrec_package.ML Thu Aug 30 22:35:34 2007 +0200
@@ -21,7 +21,7 @@
(* legacy type inference *)
fun legacy_infer_term thy t =
- singleton (ProofContext.infer_types (ProofContext.init thy)) (Sign.intern_term thy t);
+ singleton (Syntax.check_terms (ProofContext.init thy)) (Sign.intern_term thy t);
fun legacy_infer_prop thy t = legacy_infer_term thy (TypeInfer.constrain t propT);
--- a/src/Pure/Tools/invoke.ML Thu Aug 30 21:44:29 2007 +0200
+++ b/src/Pure/Tools/invoke.ML Thu Aug 30 22:35:34 2007 +0200
@@ -99,7 +99,7 @@
end;
fun infer_terms ctxt =
- ProofContext.infer_types ctxt o
+ Syntax.check_terms ctxt o
(map (fn (t, T) => TypeInfer.constrain t (TypeInfer.paramify_vars T)));
in
--- a/src/Pure/Tools/nbe.ML Thu Aug 30 21:44:29 2007 +0200
+++ b/src/Pure/Tools/nbe.ML Thu Aug 30 22:35:34 2007 +0200
@@ -137,7 +137,7 @@
^ setmp show_types true (Sign.string_of_term thy) t);
val ty = type_of t;
fun constrain t =
- singleton (ProofContext.infer_types_pats (ProofContext.init thy)) (TypeInfer.constrain t ty);
+ singleton (Syntax.check_terms (ProofContext.init thy)) (TypeInfer.constrain t ty);
val _ = ensure_funs thy funcgr t;
in
t
--- a/src/Tools/nbe.ML Thu Aug 30 21:44:29 2007 +0200
+++ b/src/Tools/nbe.ML Thu Aug 30 22:35:34 2007 +0200
@@ -323,7 +323,7 @@
subst_Frees (map (fn (s, T) => (s, Term.Free (s, T))) (Term.add_frees t []))
#> subst_Vars (map (fn (ixn, T) => (ixn, Var (ixn, T))) (Term.add_vars t []))
fun constrain t =
- singleton (ProofContext.infer_types_pats (ProofContext.init thy)) (TypeInfer.constrain t ty);
+ singleton (Syntax.check_terms (ProofContext.init thy)) (TypeInfer.constrain t ty);
fun check_tvars t = if null (Term.term_tvars t) then t else
error ("Illegal schematic type variables in normalized term: "
^ setmp show_types true (Sign.string_of_term thy) t);