src/HOL/Tools/datatype_aux.ML
changeset 18377 0e1d025d57b3
parent 18349 58de95a16d3c
child 18728 6790126ab5f6
     1.1 --- a/src/HOL/Tools/datatype_aux.ML	Thu Dec 08 20:16:17 2005 +0100
     1.2 +++ b/src/HOL/Tools/datatype_aux.ML	Fri Dec 09 09:06:45 2005 +0100
     1.3 @@ -81,21 +81,21 @@
     1.4  
     1.5  (* store theorems in theory *)
     1.6  
     1.7 -fun store_thmss_atts label tnames attss thmss thy =
     1.8 -  (thy, tnames ~~ attss ~~ thmss) |>
     1.9 -  foldl_map (fn (thy', ((tname, atts), thms)) => thy' |>
    1.10 -    Theory.add_path tname |>
    1.11 -    (apsnd hd o PureThy.add_thmss [((label, thms), atts)]) |>>
    1.12 -    Theory.parent_path) |> Library.swap;
    1.13 +fun store_thmss_atts label tnames attss thmss =
    1.14 +  fold_map (fn ((tname, atts), thms) =>
    1.15 +    Theory.add_path tname
    1.16 +    #> PureThy.add_thmss [((label, thms), atts)]
    1.17 +    #-> (fn thm::_ => Theory.parent_path #> pair thm)
    1.18 +  ) (tnames ~~ attss ~~ thmss);
    1.19  
    1.20  fun store_thmss label tnames = store_thmss_atts label tnames (replicate (length tnames) []);
    1.21  
    1.22 -fun store_thms_atts label tnames attss thms thy =
    1.23 -  (thy, tnames ~~ attss ~~ thms) |>
    1.24 -  foldl_map (fn (thy', ((tname, atts), thm)) => thy' |>
    1.25 -    Theory.add_path tname |>
    1.26 -    (apsnd hd o PureThy.add_thms [((label, thm), atts)]) |>>
    1.27 -    Theory.parent_path) |> Library.swap;
    1.28 +fun store_thms_atts label tnames attss thmss =
    1.29 +  fold_map (fn ((tname, atts), thms) =>
    1.30 +    Theory.add_path tname
    1.31 +    #> PureThy.add_thms [((label, thms), atts)]
    1.32 +    #-> (fn thm::_ => Theory.parent_path #> pair thm)
    1.33 +  ) (tnames ~~ attss ~~ thmss);
    1.34  
    1.35  fun store_thms label tnames = store_thms_atts label tnames (replicate (length tnames) []);
    1.36