src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML

 
         val ((_, [{cong_intro_pairs, coinduct, coinduct_attrs}]), lthy) = lthy
           |> derive_and_update_coinduct_cong_intross [corec_info];
         val cong_intros_pairs = AList.group (op =) cong_intro_pairs;
 
-        val code_attrs = if plugins code_plugin then [Code.add_default_eqn_attrib Code.Equation] else [];
-
         val anonymous_notes = [];
 (* TODO:
           [(flat disc_iff_or_disc_thmss, simp_attrs)]
           |> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])]));
 *)
 
         val notes =
           [(cong_introsN, maps snd cong_intros_pairs, []),
-           (codeN, [code_thm], code_attrs @ nitpicksimp_attrs),
+           (codeN, [code_thm], nitpicksimp_attrs),
            (coinductN, [coinduct], coinduct_attrs),
            (inner_inductN, inner_fp_inducts, []),
            (uniqueN, uniques, [])] @
            map (fn (thmN, thms) => (thmN, thms, [])) cong_intros_pairs @
           (if Config.get lthy bnf_internals then

 (* TODO:
         |> Spec_Rules.add Spec_Rules.Equational ([fun_t0], flat sel_thmss)
         |> Spec_Rules.add Spec_Rules.Equational ([fun_t0], flat ctr_thmss)
 *)
         |> Spec_Rules.add Spec_Rules.Equational ([fun_t0], [code_thm])
+        |> plugins code_plugin ? Code.declare_default_eqns [(code_thm, true)]
         |> Local_Theory.notes (anonymous_notes @ notes)
         |> snd
       end;
 
     fun prove_transfer_goal ctxt goal =