diff -r 1a9ac371e5a0 -r 9608028d8f43 src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Mon Sep 01 16:17:47 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Mon Sep 01 16:17:47 2014 +0200
@@ -377,7 +377,7 @@
 
     val ((missing_res_Ts, perm0_kks, fp_sugars as {fp_nesting_bnfs,
           common_co_inducts = common_coinduct_thms, ...} :: _, (_, gfp_sugar_thms)), lthy) =
-      nested_to_mutual_fps Greatest_FP bs res_Ts callers callssss0 lthy0;
+      nested_to_mutual_fps Greatest_FP true bs res_Ts callers callssss0 lthy0;
 
     val perm_fp_sugars = sort (int_ord o pairself #fp_res_index) fp_sugars;