diff -r 7553a1bcecb7 -r a5a3b576fcfb src/HOL/Tools/BNF/bnf_lfp_compat.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Sun Sep 14 22:59:30 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Mon Sep 15 10:49:07 2014 +0200
@@ -286,7 +286,8 @@
 
     val ((fp_sugars', (lfp_sugar_thms', _)), lthy') =
       if nn > nn_fp then
-        mutualize_fp_sugars Least_FP cliques compat_bs fpTs' callers callssss fp_sugars lthy
+        mutualize_fp_sugars (K true) Least_FP cliques compat_bs fpTs' callers callssss fp_sugars
+          lthy
       else
         ((fp_sugars, (NONE, NONE)), lthy);