diff -r 1a9ac371e5a0 -r 9608028d8f43 src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML	Mon Sep 01 16:17:47 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML	Mon Sep 01 16:17:47 2014 +0200
@@ -31,7 +31,7 @@
     val ((missing_arg_Ts, perm0_kks,
           fp_sugars as {fp_nesting_bnfs, common_co_inducts = [common_induct], ...} :: _,
           (lfp_sugar_thms, _)), lthy) =
-      nested_to_mutual_fps Least_FP bs arg_Ts callers callssss0 lthy0;
+      nested_to_mutual_fps Least_FP true bs arg_Ts callers callssss0 lthy0;
 
     val Ts = map #T fp_sugars;
     val Xs = map #X fp_sugars;