src/HOL/Tools/datatype_package.ML
changeset 17084 fb0a80aef0be
parent 17057 0934ac31985f
child 17261 193b84a70ca4
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Tue Aug 16 13:54:24 2005 +0200
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Tue Aug 16 15:36:28 2005 +0200
     1.3 @@ -281,6 +281,9 @@
     1.4  
     1.5  end;
     1.6  
     1.7 +fun name_notE th =
     1.8 +    Thm.name_thm (Thm.name_of_thm th ^ "_E", th RS notE);
     1.9 +      
    1.10  fun add_rules simps case_thms size_thms rec_thms inject distinct
    1.11                    weak_case_congs cong_att =
    1.12    (#1 o PureThy.add_thmss [(("simps", simps), []),
    1.13 @@ -288,7 +291,7 @@
    1.14            List.concat distinct  @ rec_thms), [Simplifier.simp_add_global]),
    1.15      (("", size_thms @ rec_thms),             [RecfunCodegen.add NONE]),
    1.16      (("", List.concat inject),               [iff_add_global]),
    1.17 -    (("", List.concat distinct RL [notE]),   [Classical.safe_elim_global]),
    1.18 +    (("", map name_notE (List.concat distinct)),  [Classical.safe_elim_global]),
    1.19      (("", weak_case_congs),                  [cong_att])]);
    1.20  
    1.21