# HG changeset patch
# User wenzelm
# Date 1190660858 -7200
# Node ID fe88913f3706669c819a7eeb7d684fd0c799d68a
# Parent  a5d89a87e8e3e1fe1bb7d0a436ee0944f7e964a3
eliminated ProofContext.read_termTs;

diff -r a5d89a87e8e3 -r fe88913f3706 src/HOL/Tools/function_package/fundef_core.ML
--- 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
 
diff -r a5d89a87e8e3 -r fe88913f3706 src/Pure/Isar/locale.ML
--- 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);
 
diff -r a5d89a87e8e3 -r fe88913f3706 src/Pure/Isar/proof_context.ML
--- 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;
 
 
diff -r a5d89a87e8e3 -r fe88913f3706 src/Pure/Tools/invoke.ML
--- 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;