# HG changeset patch
# User oheimb
# Date 991320740 -7200
# Node ID cd605c85e421080c1e99c4bcf4b8e98ce924f681
# Parent  57b7ad51971c05a7ab884544a2e0d0a22fb1b18d
improved iff_add_global, new function add_rules factoring out common behaviour

diff -r 57b7ad51971c -r cd605c85e421 src/HOL/Tools/datatype_package.ML
--- a/src/HOL/Tools/datatype_package.ML	Thu May 31 16:52:02 2001 +0200
+++ b/src/HOL/Tools/datatype_package.ML	Thu May 31 16:52:20 2001 +0200
@@ -285,6 +285,15 @@
 
 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 *)
 
@@ -570,10 +579,8 @@
 
     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 |>
@@ -628,10 +635,8 @@
 
     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 |>
@@ -734,10 +739,8 @@
     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 |>