src/HOL/Tools/datatype_aux.ML
changeset 18314 4595eb4627fa
parent 18145 6757627acf59
child 18319 c52b139ebde0
     1.1 --- a/src/HOL/Tools/datatype_aux.ML	Thu Dec 01 06:28:41 2005 +0100
     1.2 +++ b/src/HOL/Tools/datatype_aux.ML	Thu Dec 01 08:28:02 2005 +0100
     1.3 @@ -15,12 +15,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_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_thmss : string -> string list -> thm list list -> theory -> thm list list * theory
    1.11    val store_thms_atts : string -> string list -> theory attribute list list -> thm list
    1.12 -    -> theory -> theory * thm list
    1.13 -  val store_thms : string -> string list -> thm list -> theory -> theory * thm list
    1.14 +    -> theory -> thm list * theory
    1.15 +  val store_thms : string -> string list -> thm list -> theory -> thm list * theory
    1.16  
    1.17    val split_conj_thm : thm -> thm list
    1.18    val mk_conj : term list -> term
    1.19 @@ -86,7 +84,7 @@
    1.20    foldl_map (fn (thy', ((tname, atts), thms)) => thy' |>
    1.21      Theory.add_path tname |>
    1.22      (apsnd hd o PureThy.add_thmss [((label, thms), atts)]) |>>
    1.23 -    Theory.parent_path);
    1.24 +    Theory.parent_path) |> Library.swap;
    1.25  
    1.26  fun store_thmss label tnames = store_thmss_atts label tnames (replicate (length tnames) []);
    1.27  
    1.28 @@ -95,7 +93,7 @@
    1.29    foldl_map (fn (thy', ((tname, atts), thm)) => thy' |>
    1.30      Theory.add_path tname |>
    1.31      (apsnd hd o PureThy.add_thms [((label, thm), atts)]) |>>
    1.32 -    Theory.parent_path);
    1.33 +    Theory.parent_path) |> Library.swap;
    1.34  
    1.35  fun store_thms label tnames = store_thms_atts label tnames (replicate (length tnames) []);
    1.36