# HG changeset patch
# User wenzelm
# Date 952950151 -3600
# Node ID 51a040fd2200f7b1695814ec53ff43161ab4bfd7
# Parent  5e4bba59bfaa9bab3a4c4d3c685e3995e97c3917
adapted to new PureThy.add_thms etc.;
added store_thms_atts;

diff -r 5e4bba59bfaa -r 51a040fd2200 src/HOL/Tools/datatype_aux.ML
--- a/src/HOL/Tools/datatype_aux.ML	Mon Mar 13 13:21:39 2000 +0100
+++ b/src/HOL/Tools/datatype_aux.ML	Mon Mar 13 13:22:31 2000 +0100
@@ -16,8 +16,10 @@
   val add_path : bool -> string -> theory -> theory
   val parent_path : bool -> theory -> theory
 
-  val store_thmss : string -> string list -> thm list list -> theory -> theory
-  val store_thms : string -> string list -> thm list -> theory -> theory
+  val store_thmss : string -> string list -> thm list list -> theory -> theory * thm list list
+  val store_thms_atts : string -> string list -> theory attribute list list -> thm list
+    -> theory -> theory * thm list
+  val store_thms : string -> string list -> thm list -> theory -> theory * thm list
 
   val split_conj_thm : thm -> thm list
   val mk_conj : term list -> term
@@ -74,21 +76,25 @@
 fun add_path flat_names s = if flat_names then I else Theory.add_path s;
 fun parent_path flat_names = if flat_names then I else Theory.parent_path;
 
+
 (* store theorems in theory *)
 
 fun store_thmss label tnames thmss thy =
-  foldr (fn ((tname, thms), thy') => thy' |>
+  (thy, tnames ~~ thmss) |>
+  foldl_map (fn (thy', (tname, thms)) => thy' |>
     Theory.add_path tname |>
-    PureThy.add_thmss [((label, thms), [])] |>
-    Theory.parent_path)
-      (tnames ~~ thmss, thy);
+    (apsnd hd o PureThy.add_thmss [((label, thms), [])]) |>>
+    Theory.parent_path);
 
-fun store_thms label tnames thms thy =
-  foldr (fn ((tname, thm), thy') => thy' |>
+fun store_thms_atts label tnames attss thms thy =
+  (thy, tnames ~~ attss ~~ thms) |>
+  foldl_map (fn (thy', ((tname, atts), thm)) => thy' |>
     Theory.add_path tname |>
-    PureThy.add_thms [((label, thm), [])] |>
-    Theory.parent_path)
-      (tnames ~~ thms, thy);
+    (apsnd hd o PureThy.add_thms [((label, thm), atts)]) |>>
+    Theory.parent_path);
+
+fun store_thms label tnames = store_thms_atts label tnames (replicate (length tnames) []);
+
 
 (* split theorem thm_1 & ... & thm_n into n theorems *)