diff -r 219e543496a3 -r 25565bbbd246 src/HOL/Tools/inductive_package.ML
--- a/src/HOL/Tools/inductive_package.ML	Fri Nov 09 22:50:32 2001 +0100
+++ b/src/HOL/Tools/inductive_package.ML	Fri Nov 09 22:50:58 2001 +0100
@@ -858,9 +858,9 @@
     val intr_atts = map (map (Attrib.global_attribute thy) o snd) intro_srcs;
     val (cs', intr_ts') = unify_consts sign cs intr_ts;
 
-    val ((thy', con_defs), monos) = thy
+    val (thy', (monos, con_defs)) = thy
       |> IsarThy.apply_theorems raw_monos
-      |> apfst (IsarThy.apply_theorems raw_con_defs);
+      |>>> IsarThy.apply_theorems raw_con_defs;
   in
     add_inductive_i verbose false "" coind false false cs'
       ((intr_names ~~ intr_ts') ~~ intr_atts) monos con_defs thy'