src/HOL/Tools/datatype_package.ML
changeset 18690 16a64bdc5485
parent 18688 abf0f018b5ec
child 18702 7dc7dcd63224
--- 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])]);