# HG changeset patch
# User wenzelm
# Date 1213808110 -7200
# Node ID 5b3101338f421ab61613b35d3ea8b297741d7305
# Parent  17d617c6b026cce2088e2742aa5ec6f27b6d22b8
eliminated old Sign.read_term/Thm.read_cterm etc.;

diff -r 17d617c6b026 -r 5b3101338f42 src/HOL/Tools/datatype_package.ML
--- a/src/HOL/Tools/datatype_package.ML	Wed Jun 18 18:55:08 2008 +0200
+++ b/src/HOL/Tools/datatype_package.ML	Wed Jun 18 18:55:10 2008 +0200
@@ -544,7 +544,7 @@
   end;
 
 val rep_datatype = gen_rep_datatype Sign.cert_term;
-val rep_datatype_cmd = gen_rep_datatype Sign.read_term (K I);
+val rep_datatype_cmd = gen_rep_datatype Syntax.read_term_global (K I);
 
 
 
diff -r 17d617c6b026 -r 5b3101338f42 src/ZF/Tools/datatype_package.ML
--- a/src/ZF/Tools/datatype_package.ML	Wed Jun 18 18:55:08 2008 +0200
+++ b/src/ZF/Tools/datatype_package.ML	Wed Jun 18 18:55:10 2008 +0200
@@ -405,12 +405,15 @@
 fun add_datatype (sdom, srec_tms) scon_ty_lists (raw_monos, raw_type_intrs, raw_type_elims) thy =
   let
     val ctxt = ProofContext.init thy;
-    val read_i = Sign.simple_read_term thy @{typ i};
-    val rec_tms = map read_i srec_tms;
-    val con_ty_lists = Ind_Syntax.read_constructs thy scon_ty_lists;
+    fun read_is strs =
+      map (Syntax.parse_term ctxt #> TypeInfer.constrain @{typ i}) strs
+      |> Syntax.check_terms ctxt;
+
+    val rec_tms = read_is srec_tms;
+    val con_ty_lists = Ind_Syntax.read_constructs ctxt scon_ty_lists;
     val dom_sum =
       if sdom = "" then data_domain coind (rec_tms, con_ty_lists)
-      else read_i sdom;
+      else singleton read_is sdom;
     val monos = Attrib.eval_thms ctxt raw_monos;
     val type_intrs = Attrib.eval_thms ctxt raw_type_intrs;
     val type_elims = Attrib.eval_thms ctxt raw_type_elims;
diff -r 17d617c6b026 -r 5b3101338f42 src/ZF/Tools/inductive_package.ML
--- a/src/ZF/Tools/inductive_package.ML	Wed Jun 18 18:55:08 2008 +0200
+++ b/src/ZF/Tools/inductive_package.ML	Wed Jun 18 18:55:10 2008 +0200
@@ -277,7 +277,8 @@
       (Thm.assume A RS elim)
       |> Drule.standard';
   fun mk_cases a = make_cases (*delayed evaluation of body!*)
-    (simpset ()) (Thm.read_cterm (Thm.theory_of_thm elim) (a, propT));
+    (simpset ())
+    let val thy = Thm.theory_of_thm elim in cterm_of thy (Syntax.read_prop_global thy a) end;
 
   fun induction_rules raw_induct thy =
    let
diff -r 17d617c6b026 -r 5b3101338f42 src/ZF/ind_syntax.ML
--- a/src/ZF/ind_syntax.ML	Wed Jun 18 18:55:08 2008 +0200
+++ b/src/ZF/ind_syntax.ML	Wed Jun 18 18:55:10 2008 +0200
@@ -66,8 +66,9 @@
   | dest_mem _ = error "Constructor specifications must have the form x:A";
 
 (*read a constructor specification*)
-fun read_construct sign (id, sprems, syn) =
-    let val prems = map (Sign.simple_read_term sign FOLogic.oT) sprems
+fun read_construct ctxt (id, sprems, syn) =
+    let val prems = map (Syntax.parse_term ctxt #> TypeInfer.constrain FOLogic.oT) sprems
+          |> Syntax.check_terms ctxt
         val args = map (#1 o dest_mem) prems
         val T = (map (#2 o dest_Free) args) ---> iT
                 handle TERM _ => error