New function store_thmss_atts.
--- 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' |>