src/HOL/Tools/datatype_aux.ML
changeset 18101 43724981f8f9
parent 18069 f2c8f68a45e6
child 18145 6757627acf59
     1.1 --- a/src/HOL/Tools/datatype_aux.ML	Mon Nov 07 11:17:45 2005 +0100
     1.2 +++ b/src/HOL/Tools/datatype_aux.ML	Mon Nov 07 11:28:34 2005 +0100
     1.3 @@ -15,6 +15,8 @@
     1.4    val add_path : bool -> string -> theory -> theory
     1.5    val parent_path : bool -> theory -> theory
     1.6  
     1.7 +  val store_thmss_atts : string -> string list -> theory attribute list list -> thm list list
     1.8 +    -> theory -> theory * thm list list
     1.9    val store_thmss : string -> string list -> thm list list -> theory -> theory * thm list list
    1.10    val store_thms_atts : string -> string list -> theory attribute list list -> thm list
    1.11      -> theory -> theory * thm list
    1.12 @@ -79,13 +81,15 @@
    1.13  
    1.14  (* store theorems in theory *)
    1.15  
    1.16 -fun store_thmss label tnames thmss thy =
    1.17 -  (thy, tnames ~~ thmss) |>
    1.18 -  foldl_map (fn (thy', (tname, thms)) => thy' |>
    1.19 +fun store_thmss_atts label tnames attss thmss thy =
    1.20 +  (thy, tnames ~~ attss ~~ thmss) |>
    1.21 +  foldl_map (fn (thy', ((tname, atts), thms)) => thy' |>
    1.22      Theory.add_path tname |>
    1.23 -    (apsnd hd o PureThy.add_thmss [((label, thms), [])]) |>>
    1.24 +    (apsnd hd o PureThy.add_thmss [((label, thms), atts)]) |>>
    1.25      Theory.parent_path);
    1.26  
    1.27 +fun store_thmss label tnames = store_thmss_atts label tnames (replicate (length tnames) []);
    1.28 +
    1.29  fun store_thms_atts label tnames attss thms thy =
    1.30    (thy, tnames ~~ attss ~~ thms) |>
    1.31    foldl_map (fn (thy', ((tname, atts), thm)) => thy' |>