Eliminated store_clasimp.

--- a/src/HOL/Tools/datatype_package.ML	Wed Mar 15 23:36:46 2000 +0100
+++ b/src/HOL/Tools/datatype_package.ML	Wed Mar 15 23:38:19 2000 +0100
@@ -348,9 +348,6 @@
        nchotomy = nchotomy,
        case_cong = case_cong});
 
-fun store_clasimp thy (cla, simp) =
-  (claset_ref_of thy := cla; simpset_ref_of thy := simp);
-
 
 (********************* axiomatic introduction of datatypes ********************)
 
@@ -517,15 +514,13 @@
 
     val thy11 = thy10 |>
       Theory.add_path (space_implode "_" new_type_names) |>
-      (#1 o PureThy.add_thmss [(("simps", simps), [])]) |>
+      (#1 o PureThy.add_thmss [(("simps", simps), []),
+        (("", flat case_thms @ size_thms @ rec_thms), [Simplifier.simp_add_global]),
+        (("", flat (inject @ distinct)), [iff_add_global])]) |>
       put_datatypes (foldr Symtab.update (dt_infos, dt_info)) |>
       add_cases_induct dt_infos |>
       Theory.parent_path;
 
-    val _ = store_clasimp thy11 ((claset_of thy11, simpset_of thy11)
-      addsimps2 flat case_thms addsimps2 size_thms addsimps2 rec_thms
-      addIffs flat (inject @ distinct));
-
   in
     (thy11,
      {distinct = distinct,
@@ -553,7 +548,7 @@
 
     val (thy3, casedist_thms) = DatatypeAbsProofs.prove_casedist_thms new_type_names descr
       sorts induct case_names_exhausts thy2;
-    val (thy4, reccomb_names, rec_thms) = DatatypeAbsProofs.prove_primrec_thms
+    val (thy4, (reccomb_names, rec_thms)) = DatatypeAbsProofs.prove_primrec_thms
       flat_names new_type_names descr sorts dt_info inject dist_rewrites dist_ss induct thy3;
     val (thy6, (case_thms, case_names)) = DatatypeAbsProofs.prove_case_thms
       flat_names new_type_names descr sorts reccomb_names rec_thms thy4;
@@ -574,15 +569,13 @@
 
     val thy11 = thy10 |>
       Theory.add_path (space_implode "_" new_type_names) |>
-      (#1 o PureThy.add_thmss [(("simps", simps), [])]) |>
+      (#1 o PureThy.add_thmss [(("simps", simps), []),
+        (("", flat case_thms @ size_thms @ rec_thms), [Simplifier.simp_add_global]),
+        (("", flat (inject @ distinct)), [iff_add_global])]) |>
       put_datatypes (foldr Symtab.update (dt_infos, dt_info)) |>
       add_cases_induct dt_infos |>
       Theory.parent_path;
 
-    val _ = store_clasimp thy11 ((claset_of thy11, simpset_of thy11)
-      addsimps2 flat case_thms addsimps2 size_thms addsimps2 rec_thms
-      addIffs flat (inject @ distinct));
-
   in
     (thy11,
      {distinct = distinct,
@@ -650,7 +643,7 @@
     val (thy2, casedist_thms) = thy1 |>
       DatatypeAbsProofs.prove_casedist_thms new_type_names [descr] sorts induction
         case_names_exhausts;
-    val (thy3, reccomb_names, rec_thms) = DatatypeAbsProofs.prove_primrec_thms
+    val (thy3, (reccomb_names, rec_thms)) = DatatypeAbsProofs.prove_primrec_thms
       false new_type_names [descr] sorts dt_info inject distinct dist_ss induction thy2;
     val (thy4, (case_thms, case_names)) = DatatypeAbsProofs.prove_case_thms false
       new_type_names [descr] sorts reccomb_names rec_thms thy3;
@@ -677,15 +670,13 @@
       (#1 o store_thmss "distinct" new_type_names distinct) |>
       Theory.add_path (space_implode "_" new_type_names) |>
       PureThy.add_thms [(("induct", induction), [case_names_induct])] |>>
-      (#1 o PureThy.add_thmss [(("simps", simps), [])]) |>>
+      (#1 o PureThy.add_thmss [(("simps", simps), []),
+        (("", flat case_thms @ size_thms @ rec_thms), [Simplifier.simp_add_global]),
+        (("", flat (inject @ distinct)), [iff_add_global])]) |>>
       put_datatypes (foldr Symtab.update (dt_infos, dt_info)) |>>
       add_cases_induct dt_infos |>>
       Theory.parent_path;
 
-    (* FIXME use attributes *)
-    val _ = store_clasimp thy9 ((claset_of thy9, simpset_of thy9)
-      addsimps2 flat case_thms addsimps2 size_thms addsimps2 rec_thms
-      addIffs flat (inject @ distinct));
   in
     (thy9,
      {distinct = distinct,