src/HOL/Tools/datatype_package.ML
changeset 18418 bf448d999b7e
parent 18377 0e1d025d57b3
child 18451 5ff0244e25e8
--- a/src/HOL/Tools/datatype_package.ML	Thu Dec 15 21:51:31 2005 +0100
+++ b/src/HOL/Tools/datatype_package.ML	Fri Dec 16 09:00:11 2005 +0100
@@ -766,13 +766,11 @@
   let
     val _ = Theory.requires thy0 "Inductive" "datatype representations";
 
-    fun app_thmss srcs thy = foldl_map (fn (thy, x) => apply_theorems x thy) (thy, srcs);
-    fun app_thm src thy = apsnd hd (apply_theorems [src] thy);
-
-    val (((thy1, induction), inject), distinct) = thy0
-      |> app_thmss raw_distinct
-      |> apfst (app_thmss raw_inject)
-      |> apfst (apfst (app_thm raw_induction));
+    val (((distinct, inject), [induction]), thy1) =
+      thy0
+      |> fold_map apply_theorems raw_distinct
+      ||>> fold_map apply_theorems raw_inject
+      ||>> apply_theorems [raw_induction];
     val sign = Theory.sign_of thy1;
 
     val induction' = freezeT induction;