--- a/src/HOL/Tools/function_package/fundef_core.ML Mon Sep 24 21:07:36 2007 +0200
+++ b/src/HOL/Tools/function_package/fundef_core.ML Mon Sep 24 21:07:38 2007 +0200
@@ -866,7 +866,8 @@
val domT = domain_type fT
val ranT = range_type fT
- val default = singleton (ProofContext.read_termTs lthy) (default_str, fT)
+ val default = Syntax.parse_term lthy default_str
+ |> TypeInfer.constrain fT |> Syntax.check_term lthy
val (globals, ctxt') = fix_globals domT ranT fvar lthy
--- a/src/Pure/Isar/locale.ML Mon Sep 24 21:07:36 2007 +0200
+++ b/src/Pure/Isar/locale.ML Mon Sep 24 21:07:38 2007 +0200
@@ -2080,7 +2080,7 @@
(* add witnesses of Assumed elements (only those generate proof obligations) *)
|> fold (fn (id, thms) => fold (add_wit id) thms) (map fst propss ~~ thmss)
(* add equations *)
- |> fold (fn (id, thms) => fold (add_eqn id) thms) (map fst eq_props ~~
+ |> fold (fn (id, thms) => fold (add_eqn id) thms) (map fst eq_props ~~
(map o map) (abs_eqn o LocalDefs.meta_rewrite_rule ctxt o
Element.conclude_witness) eq_thms);
@@ -2133,6 +2133,9 @@
add_local_equation
x;
+fun read_termT ctxt (t, T) =
+ Syntax.parse_term ctxt t |> TypeInfer.constrain (TypeInfer.paramify_vars T);
+
fun read_instantiations ctxt parms (insts, eqns) =
let
val thy = ProofContext.theory_of ctxt;
@@ -2149,11 +2152,9 @@
| ((x, T), SOME inst) => SOME (x, (inst, T)));
val (given_ps, given_insts) = split_list given;
- (* equations *)
- val max_eqs = length eqns;
-
(* read given insts / eqns *)
- val all_vs = ProofContext.read_termTs ctxt (given_insts @ (eqns ~~ replicate max_eqs propT));
+ val all_vs = (map (read_termT ctxt) given_insts @ map (Syntax.read_prop ctxt) eqns)
+ |> Syntax.check_terms ctxt;
val ctxt' = ctxt |> fold Variable.declare_term all_vs;
val (vs, eqns') = all_vs |> chop (length given_insts);
--- a/src/Pure/Isar/proof_context.ML Mon Sep 24 21:07:36 2007 +0200
+++ b/src/Pure/Isar/proof_context.ML Mon Sep 24 21:07:38 2007 +0200
@@ -65,7 +65,6 @@
-> (indexname -> sort option) -> string list -> (string * typ) list
-> term list * (indexname * typ) list
val read_prop_legacy: Proof.context -> string -> term
- val read_termTs: Proof.context -> (string * typ) list -> term list
val cert_term: Proof.context -> term -> term
val cert_prop: Proof.context -> term -> term
val infer_type: Proof.context -> string -> typ
@@ -543,10 +542,6 @@
fun read_prop_thy freeze pp syn thy defaults fixed s =
#1 (read_def_termT freeze pp syn thy defaults fixed (s, propT));
-fun read_terms_thy freeze pp syn thy defaults fixed =
- #1 o read_def_termTs freeze pp syn thy defaults fixed;
-
-
fun append_env e1 e2 x = (case e2 x of NONE => e1 x | some => some);
fun gen_read' read app schematic ctxt0 internal more_types more_sorts more_used s =
@@ -573,8 +568,6 @@
fun read_prop_legacy ctxt =
gen_read' (read_prop_thy true) I false ctxt (K true) (K NONE) (K NONE) [];
-val read_termTs = gen_read (read_terms_thy true) map false;
-
end;
--- a/src/Pure/Tools/invoke.ML Mon Sep 24 21:07:36 2007 +0200
+++ b/src/Pure/Tools/invoke.ML Mon Sep 24 21:07:38 2007 +0200
@@ -21,7 +21,7 @@
local
-fun gen_invoke prep_att prep_expr prep_terms add_fixes
+fun gen_invoke prep_att prep_expr parse_term add_fixes
(prfx, raw_atts) raw_expr raw_insts fixes int state =
let
val _ = Proof.assert_forward_or_chain state;
@@ -45,10 +45,11 @@
val raw_insts' = zip_options params' raw_insts
handle Library.UnequalLengths => error "Too many instantiations";
+
+ fun prep_inst (t, u) =
+ TypeInfer.constrain (TypeInfer.paramify_vars (Term.fastype_of t)) (parse_term ctxt' u);
val insts = map #1 raw_insts' ~~
- Variable.polymorphic ctxt'
- (prep_terms ctxt' (map (fn (t, u) => (u, Term.fastype_of t)) raw_insts'));
-
+ Variable.polymorphic ctxt' (Syntax.check_terms ctxt' (map prep_inst raw_insts'));
val inst_rules =
replicate (length types') Drule.termI @
map (fn t =>
@@ -98,15 +99,11 @@
|> Seq.hd
end;
-fun infer_terms ctxt =
- Syntax.check_terms ctxt o
- (map (fn (t, T) => TypeInfer.constrain (TypeInfer.paramify_vars T) t));
-
in
fun invoke x =
- gen_invoke Attrib.attribute Locale.read_expr ProofContext.read_termTs ProofContext.add_fixes x;
-fun invoke_i x = gen_invoke (K I) Locale.cert_expr infer_terms ProofContext.add_fixes_i x;
+ gen_invoke Attrib.attribute Locale.read_expr Syntax.parse_term ProofContext.add_fixes x;
+fun invoke_i x = gen_invoke (K I) Locale.cert_expr (K I) ProofContext.add_fixes_i x;
end;