src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML

--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Mon Jan 05 11:00:12 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Mon Jan 05 21:24:14 2015 +0100
@@ -83,7 +83,6 @@
 
 val nitpicksimp_attrs = @{attributes [nitpick_simp]};
 val simp_attrs = @{attributes [simp]};
-val code_nitpicksimp_attrs = Code.add_default_eqn_attrib :: nitpicksimp_attrs;
 
 exception PRIMCOREC of string * term list;
 
@@ -1413,6 +1412,8 @@
 
         val common_name = mk_common_name fun_names;
 
+        val code_attrs = if plugins code_plugin then [Code.add_default_eqn_attrib] else [];
+
         val anonymous_notes =
           [(flat disc_iff_or_disc_thmss, simp_attrs)]
           |> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])]));
@@ -1428,7 +1429,7 @@
           [(coinductN, map (if n2m then single else K []) coinduct_thms, coinduct_attrs),
            (coinduct_strongN, map (if n2m then single else K []) coinduct_strong_thms,
             coinduct_attrs),
-           (codeN, code_thmss, code_nitpicksimp_attrs),
+           (codeN, code_thmss, code_attrs @ nitpicksimp_attrs),
            (ctrN, ctr_thmss, []),
            (discN, disc_thmss, []),
            (disc_iffN, disc_iff_thmss, []),