# HG changeset patch
# User wenzelm
# Date 1137351533 -3600
# Node ID 16a64bdc548592b67e6b19672e6099381afaf13d
# Parent  a50587cd8414b881a5b86061adf519fa49f6535b
classical attributes: optional weight;

diff -r a50587cd8414 -r 16a64bdc5485 src/HOL/Tools/datatype_package.ML
--- 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])]);
 
 
diff -r a50587cd8414 -r 16a64bdc5485 src/ZF/Tools/datatype_package.ML
--- 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), []),