--- a/src/HOL/Tools/datatype_package.ML Sun Jan 15 19:58:51 2006 +0100
+++ b/src/HOL/Tools/datatype_package.ML Sun Jan 15 19:58:53 2006 +0100
@@ -353,7 +353,7 @@
List.concat distinct @ rec_thms), [Attrib.theory Simplifier.simp_add]),
(("", size_thms @ rec_thms), [RecfunCodegen.add NONE]),
(("", List.concat inject), [Attrib.theory iff_add]),
- (("", map name_notE (List.concat distinct)), [Attrib.theory Classical.safe_elim]),
+ (("", map name_notE (List.concat distinct)), [Attrib.theory (Classical.safe_elim NONE)]),
(("", weak_case_congs), [cong_att])]);
--- a/src/ZF/Tools/datatype_package.ML Sun Jan 15 19:58:51 2006 +0100
+++ b/src/ZF/Tools/datatype_package.ML Sun Jan 15 19:58:53 2006 +0100
@@ -368,7 +368,7 @@
(thy1 |> Theory.add_path big_rec_base_name
|> PureThy.add_thmss
[(("simps", simps), [Attrib.theory Simplifier.simp_add]),
- (("", intrs), [Attrib.theory Classical.safe_intro]),
+ (("", intrs), [Attrib.theory (Classical.safe_intro NONE)]),
(("con_defs", con_defs), []),
(("case_eqns", case_eqns), []),
(("recursor_eqns", recursor_eqns), []),