--- 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)]