diff -r 479a779b89a6 -r b74248961819 src/HOL/Tools/BNF/bnf_lfp_compat.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Wed Feb 12 08:35:56 2014 +0100
@@ -99,9 +99,9 @@
       else
         ((fp_sugars0, (NONE, NONE)), lthy);
 
-    val {ctr_sugars, co_inducts = [induct], co_iterss, co_iter_thmsss = iter_thmsss, ...} :: _ =
-      fp_sugars;
-    val inducts = conj_dests nn induct;
+    val {ctr_sugars, co_inducts = [induct], co_inductss = inductss, co_iterss,
+      co_iter_thmsss = iter_thmsss, ...} :: _ = fp_sugars;
+    val inducts = map the_single inductss;
 
     val mk_dtyp = dtyp_of_typ Ts;