src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML

         val simp_thmss = map2 append disc_iff_or_disc_thmss sel_thmss;
 
         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)]
           |> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])]));