src/HOL/Tools/datatype_aux.ML
changeset 8435 51a040fd2200
parent 8404 4b39358f9810
child 9740 1c5b0f27de56
     1.1 --- a/src/HOL/Tools/datatype_aux.ML	Mon Mar 13 13:21:39 2000 +0100
     1.2 +++ b/src/HOL/Tools/datatype_aux.ML	Mon Mar 13 13:22:31 2000 +0100
     1.3 @@ -16,8 +16,10 @@
     1.4    val add_path : bool -> string -> theory -> theory
     1.5    val parent_path : bool -> theory -> theory
     1.6  
     1.7 -  val store_thmss : string -> string list -> thm list list -> theory -> theory
     1.8 -  val store_thms : string -> string list -> thm list -> theory -> theory
     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 +  val store_thms : string -> string list -> thm list -> theory -> theory * thm list
    1.13  
    1.14    val split_conj_thm : thm -> thm list
    1.15    val mk_conj : term list -> term
    1.16 @@ -74,21 +76,25 @@
    1.17  fun add_path flat_names s = if flat_names then I else Theory.add_path s;
    1.18  fun parent_path flat_names = if flat_names then I else Theory.parent_path;
    1.19  
    1.20 +
    1.21  (* store theorems in theory *)
    1.22  
    1.23  fun store_thmss label tnames thmss thy =
    1.24 -  foldr (fn ((tname, thms), thy') => thy' |>
    1.25 +  (thy, tnames ~~ thmss) |>
    1.26 +  foldl_map (fn (thy', (tname, thms)) => thy' |>
    1.27      Theory.add_path tname |>
    1.28 -    PureThy.add_thmss [((label, thms), [])] |>
    1.29 -    Theory.parent_path)
    1.30 -      (tnames ~~ thmss, thy);
    1.31 +    (apsnd hd o PureThy.add_thmss [((label, thms), [])]) |>>
    1.32 +    Theory.parent_path);
    1.33  
    1.34 -fun store_thms label tnames thms thy =
    1.35 -  foldr (fn ((tname, thm), thy') => thy' |>
    1.36 +fun store_thms_atts label tnames attss thms thy =
    1.37 +  (thy, tnames ~~ attss ~~ thms) |>
    1.38 +  foldl_map (fn (thy', ((tname, atts), thm)) => thy' |>
    1.39      Theory.add_path tname |>
    1.40 -    PureThy.add_thms [((label, thm), [])] |>
    1.41 -    Theory.parent_path)
    1.42 -      (tnames ~~ thms, thy);
    1.43 +    (apsnd hd o PureThy.add_thms [((label, thm), atts)]) |>>
    1.44 +    Theory.parent_path);
    1.45 +
    1.46 +fun store_thms label tnames = store_thms_atts label tnames (replicate (length tnames) []);
    1.47 +
    1.48  
    1.49  (* split theorem thm_1 & ... & thm_n into n theorems *)
    1.50