src/HOL/Tools/datatype_package.ML

   map (RuleCases.case_names o exhaust_cases descr o #1)
     (filter (fn ((_, (name, _, _))) => name mem_string new) descr);
 
 end;
 
+fun add_rules simps case_thms size_thms rec_thms inject distinct
+                  weak_case_congs cong_att =
+  (#1 o PureThy.add_thmss [(("simps", simps), []),
+    (("", flat case_thms @ size_thms @ 
+          flat distinct  @ rec_thms), [Simplifier.simp_add_global]),
+    (("", flat inject),               [iff_add_global]),
+    (("", flat distinct RL [notE]),   [Classical.safe_elim_global]),
+    (("", weak_case_congs),           [cong_att])]);
+
 
 (* add_cases_induct *)
 
 fun add_cases_induct infos =
   let

     val simps = flat (distinct @ inject @ case_thms) @ size_thms @ rec_thms;
     val split_thms = split ~~ split_asm;
 
     val thy12 = thy11 |>
       Theory.add_path (space_implode "_" new_type_names) |>
-      (#1 o PureThy.add_thmss [(("simps", simps), []),
-        (("", flat case_thms @ size_thms @ rec_thms), [Simplifier.simp_add_global]),
-        (("", flat (inject @ distinct)), [iff_add_global]),
-        (("", weak_case_congs), [Simplifier.cong_add_global])]) |>
+      add_rules simps case_thms size_thms rec_thms inject distinct
+                weak_case_congs Simplifier.cong_add_global |> 
       put_datatypes (foldr Symtab.update (dt_infos, dt_info)) |>
       add_cases_induct dt_infos |>
       Theory.parent_path |>
       (#1 o store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms));
   in

 
     val simps = flat (distinct @ inject @ case_thms) @ size_thms @ rec_thms;
 
     val thy12 = thy11 |>
       Theory.add_path (space_implode "_" new_type_names) |>
-      (#1 o PureThy.add_thmss [(("simps", simps), []),
-        (("", flat case_thms @ size_thms @ rec_thms), [Simplifier.simp_add_global]),
-        (("", flat (inject @ distinct)), [iff_add_global]),
-        (("", weak_case_congs), [Simplifier.change_global_ss (op addcongs)])]) |>
+      add_rules simps case_thms size_thms rec_thms inject distinct
+                weak_case_congs (Simplifier.change_global_ss (op addcongs)) |> 
       put_datatypes (foldr Symtab.update (dt_infos, dt_info)) |>
       add_cases_induct dt_infos |>
       Theory.parent_path |>
       (#1 o store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms));
   in

         map FewConstrs distinct ~~ inject ~~ nchotomys ~~ case_congs ~~ weak_case_congs);
 
     val simps = flat (distinct @ inject @ case_thms) @ size_thms @ rec_thms;
 
     val thy11 = thy10 |>
-      (#1 o PureThy.add_thmss [(("simps", simps), []),
-        (("", flat case_thms @ size_thms @ rec_thms), [Simplifier.simp_add_global]),
-        (("", flat (inject @ distinct)), [iff_add_global]),
-        (("", weak_case_congs), [Simplifier.change_global_ss (op addcongs)])]) |>
+      add_rules simps case_thms size_thms rec_thms inject distinct
+                weak_case_congs (Simplifier.change_global_ss (op addcongs)) |> 
       put_datatypes (foldr Symtab.update (dt_infos, dt_info)) |>
       add_cases_induct dt_infos |>
       Theory.parent_path |>
       (#1 o store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms));
   in