src/HOL/Tools/datatype_package.ML
changeset 18690 16a64bdc5485
parent 18688 abf0f018b5ec
child 18702 7dc7dcd63224
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Sun Jan 15 19:58:51 2006 +0100
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Sun Jan 15 19:58:53 2006 +0100
     1.3 @@ -353,7 +353,7 @@
     1.4            List.concat distinct  @ rec_thms), [Attrib.theory Simplifier.simp_add]),
     1.5      (("", size_thms @ rec_thms),             [RecfunCodegen.add NONE]),
     1.6      (("", List.concat inject),               [Attrib.theory iff_add]),
     1.7 -    (("", map name_notE (List.concat distinct)),  [Attrib.theory Classical.safe_elim]),
     1.8 +    (("", map name_notE (List.concat distinct)),  [Attrib.theory (Classical.safe_elim NONE)]),
     1.9      (("", weak_case_congs),                  [cong_att])]);
    1.10  
    1.11