# HG changeset patch
# User wenzelm
# Date 1190827081 -7200
# Node ID fcf13a91cda2a428925d509421534f9b89bbb827
# Parent  04b676d1a1fe1962ebfb3b2919d583484bb38cb9
Attrib.eval_thms;
Syntax.parse/check;

diff -r 04b676d1a1fe -r fcf13a91cda2 src/ZF/Tools/inductive_package.ML
--- a/src/ZF/Tools/inductive_package.ML	Wed Sep 26 19:18:00 2007 +0200
+++ b/src/ZF/Tools/inductive_package.ML	Wed Sep 26 19:18:01 2007 +0200
@@ -552,22 +552,23 @@
 fun add_inductive (srec_tms, sdom_sum) intr_srcs
     (raw_monos, raw_con_defs, raw_type_intrs, raw_type_elims) thy =
   let
+    val ctxt = ProofContext.init thy;
+    val read_terms = map (Syntax.parse_term ctxt #> TypeInfer.constrain Ind_Syntax.iT)
+      #> Syntax.check_terms ctxt;
+
     val intr_atts = map (map (Attrib.attribute thy) o snd) intr_srcs;
     val sintrs = map fst intr_srcs ~~ intr_atts;
-    val read = Sign.simple_read_term thy;
-    val rec_tms = map (read Ind_Syntax.iT) srec_tms;
-    val dom_sum = read Ind_Syntax.iT sdom_sum;
-    val intr_tms = map (read propT o snd o fst) sintrs;
+    val rec_tms = read_terms srec_tms;
+    val dom_sum = singleton read_terms sdom_sum;
+    val intr_tms = Syntax.read_props ctxt (map (snd o fst) sintrs);
     val intr_specs = (map (fst o fst) sintrs ~~ intr_tms) ~~ map snd sintrs;
+    val monos = Attrib.eval_thms ctxt raw_monos;
+    val con_defs = Attrib.eval_thms ctxt raw_con_defs;
+    val type_intrs = Attrib.eval_thms ctxt raw_type_intrs;
+    val type_elims = Attrib.eval_thms ctxt raw_type_elims;
   in
     thy
-    |> IsarCmd.apply_theorems raw_monos
-    ||>> IsarCmd.apply_theorems raw_con_defs
-    ||>> IsarCmd.apply_theorems raw_type_intrs
-    ||>> IsarCmd.apply_theorems raw_type_elims
-    |-> (fn (((monos, con_defs), type_intrs), type_elims) =>
-          add_inductive_i true (rec_tms, dom_sum) intr_specs
-            (monos, con_defs, type_intrs, type_elims))
+    |> add_inductive_i true (rec_tms, dom_sum) intr_specs (monos, con_defs, type_intrs, type_elims)
   end;