diff -r 7c593d4f1f89 -r d562c9948dee src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Mon Jun 06 21:28:45 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Mon Jun 06 21:28:46 2016 +0200
@@ -1522,7 +1522,7 @@
         val common_name = mk_common_name fun_names;
         val common_qualify = fold_rev I qualifys;
 
-        val code_attrs = if plugins code_plugin then [Code.add_default_eqn_attrib] else [];
+        val code_attrs = if plugins code_plugin then [Code.add_default_eqn_attrib Code.Equation] else [];
 
         val anonymous_notes =
           [(flat disc_iff_or_disc_thmss, simp_attrs)]