diff -r 2ef0183fa20b -r 0e1d025d57b3 src/HOL/Tools/datatype_aux.ML
--- a/src/HOL/Tools/datatype_aux.ML	Thu Dec 08 20:16:17 2005 +0100
+++ b/src/HOL/Tools/datatype_aux.ML	Fri Dec 09 09:06:45 2005 +0100
@@ -81,21 +81,21 @@
 
 (* store theorems in theory *)
 
-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), atts)]) |>>
-    Theory.parent_path) |> Library.swap;
+fun store_thmss_atts label tnames attss thmss =
+  fold_map (fn ((tname, atts), thms) =>
+    Theory.add_path tname
+    #> PureThy.add_thmss [((label, thms), atts)]
+    #-> (fn thm::_ => Theory.parent_path #> pair thm)
+  ) (tnames ~~ attss ~~ thmss);
 
 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' |>
-    Theory.add_path tname |>
-    (apsnd hd o PureThy.add_thms [((label, thm), atts)]) |>>
-    Theory.parent_path) |> Library.swap;
+fun store_thms_atts label tnames attss thmss =
+  fold_map (fn ((tname, atts), thms) =>
+    Theory.add_path tname
+    #> PureThy.add_thms [((label, thms), atts)]
+    #-> (fn thm::_ => Theory.parent_path #> pair thm)
+  ) (tnames ~~ attss ~~ thmss);
 
 fun store_thms label tnames = store_thms_atts label tnames (replicate (length tnames) []);