# HG changeset patch
# User berghofe
# Date 1131359314 -3600
# Node ID 43724981f8f9b86f6889abf06d0e1a629b544533
# Parent  193c3382bbfeaa0955ac6190ba43e2fa22aed14d
New function store_thmss_atts.

diff -r 193c3382bbfe -r 43724981f8f9 src/HOL/Tools/datatype_aux.ML
--- a/src/HOL/Tools/datatype_aux.ML	Mon Nov 07 11:17:45 2005 +0100
+++ b/src/HOL/Tools/datatype_aux.ML	Mon Nov 07 11:28:34 2005 +0100
@@ -15,6 +15,8 @@
   val add_path : bool -> string -> theory -> theory
   val parent_path : bool -> theory -> theory
 
+  val store_thmss_atts : string -> string list -> theory attribute list list -> thm list list
+    -> theory -> theory * thm list list
   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
@@ -79,13 +81,15 @@
 
 (* store theorems in theory *)
 
-fun store_thmss label tnames thmss thy =
-  (thy, tnames ~~ thmss) |>
-  foldl_map (fn (thy', (tname, thms)) => thy' |>
+fun store_thmss_atts label tnames attss thmss thy =
+  (thy, tnames ~~ attss ~~ thmss) |>
+  foldl_map (fn (thy', ((tname, atts), thms)) => thy' |>
     Theory.add_path tname |>
-    (apsnd hd o PureThy.add_thmss [((label, thms), [])]) |>>
+    (apsnd hd o PureThy.add_thmss [((label, thms), atts)]) |>>
     Theory.parent_path);
 
+fun store_thmss label tnames = store_thmss_atts label tnames (replicate (length tnames) []);
+
 fun store_thms_atts label tnames attss thms thy =
   (thy, tnames ~~ attss ~~ thms) |>
   foldl_map (fn (thy', ((tname, atts), thm)) => thy' |>