# HG changeset patch
# User wenzelm
# Date 1190827080 -7200
# Node ID 04b676d1a1fe1962ebfb3b2919d583484bb38cb9
# Parent  0df74bb87a13d22863932be7b82e8c939b2ce45b
Attrib.eval_thms;

diff -r 0df74bb87a13 -r 04b676d1a1fe src/ZF/Tools/datatype_package.ML
--- a/src/ZF/Tools/datatype_package.ML	Wed Sep 26 19:17:59 2007 +0200
+++ b/src/ZF/Tools/datatype_package.ML	Wed Sep 26 19:18:00 2007 +0200
@@ -388,20 +388,18 @@
 
 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 Ind_Syntax.iT;
     val rec_tms = map read_i srec_tms;
     val con_ty_lists = Ind_Syntax.read_constructs thy scon_ty_lists;
     val dom_sum =
       if sdom = "" then Ind_Syntax.data_domain coind (rec_tms, con_ty_lists)
       else read_i sdom;
-  in
-    thy
-    |> IsarCmd.apply_theorems raw_monos
-    ||>> IsarCmd.apply_theorems raw_type_intrs
-    ||>> IsarCmd.apply_theorems raw_type_elims
-    |-> (fn ((monos, type_intrs), type_elims) =>
-          add_datatype_i (dom_sum, rec_tms) con_ty_lists (monos, type_intrs, type_elims))
-  end;
+    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;
+  in add_datatype_i (dom_sum, rec_tms) con_ty_lists (monos, type_intrs, type_elims) thy end;
+
 
 (* outer syntax *)
 
diff -r 0df74bb87a13 -r 04b676d1a1fe src/ZF/Tools/induct_tacs.ML
--- a/src/ZF/Tools/induct_tacs.ML	Wed Sep 26 19:17:59 2007 +0200
+++ b/src/ZF/Tools/induct_tacs.ML	Wed Sep 26 19:18:00 2007 +0200
@@ -165,14 +165,13 @@
   end;
 
 fun rep_datatype raw_elim raw_induct raw_case_eqns raw_recursor_eqns thy =
-  thy
-  |> IsarCmd.apply_theorems [raw_elim]
-  ||>> IsarCmd.apply_theorems [raw_induct]
-  ||>> IsarCmd.apply_theorems raw_case_eqns
-  ||>> IsarCmd.apply_theorems raw_recursor_eqns
-  |-> (fn (((elims, inducts), case_eqns), recursor_eqns) =>
-          rep_datatype_i (PureThy.single_thm "elimination" elims)
-            (PureThy.single_thm "induction" inducts) case_eqns recursor_eqns);
+  let
+    val ctxt = ProofContext.init thy;
+    val elim = PureThy.single_thm "elimination" (Attrib.eval_thms ctxt [raw_elim]);
+    val induct = PureThy.single_thm "induction" (Attrib.eval_thms ctxt [raw_induct]);
+    val case_eqns = Attrib.eval_thms ctxt raw_case_eqns;
+    val recursor_eqns = Attrib.eval_thms ctxt raw_recursor_eqns;
+  in rep_datatype_i elim induct case_eqns recursor_eqns thy end;
 
 
 (* theory setup *)