diff -r 32145985352a -r ac836bcddb3b src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Mon Nov 24 12:35:13 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Mon Nov 24 12:35:13 2014 +0100
@@ -385,8 +385,8 @@
           not_co_datatype0 T
       | not_co_datatype T = not_co_datatype0 T;
     fun not_mutually_nested_rec Ts1 Ts2 =
-      error (qsotys Ts1 ^ " is neither mutually recursive with " ^ qsotys Ts2 ^
-        " nor nested recursive through " ^
+      error (qsotys Ts1 ^ " is neither mutually " ^ co_prefix fp ^ "recursive with " ^ qsotys Ts2 ^
+        " nor nested " ^ co_prefix fp ^ "recursive through " ^
         (if Ts1 = Ts2 andalso length Ts1 = 1 then "itself" else qsotys Ts2));
 
     val sorted_actual_Ts =