src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML

     val plugins = get_first (fn Plugins_Option f => SOME (f lthy) | _ => NONE) (rev opts)
       |> the_default Plugin_Name.default_filter;
     val nonexhaustive = exists (can (fn Nonexhaustive_Option => ())) opts;
     val transfer = exists (can (fn Transfer_Option => ())) opts;
 
-    val code_attrs = if plugins code_plugin then [Code.add_default_eqn_attrib Code.Equation] else [];
-
     val (fixes, specs) = fst (prep_spec raw_fixes raw_specs lthy);
 
     val mk_notes =
       flat oooo @{map 4} (fn js => fn prefix => fn qualify => fn thms =>
         let
           val (bs, attrss) = map_split (fst o nth specs) js;
           val notes =
             @{map 3} (fn b => fn attrs => fn thm =>
-                ((Binding.qualify false prefix b, code_attrs @ nitpicksimp_simp_attrs @ attrs),
+                ((Binding.qualify false prefix b, nitpicksimp_simp_attrs @ attrs),
                  [([thm], [])]))
               bs attrss thms;
         in
           ((qualify (Binding.qualify true prefix (Binding.name simpsN)), []), [(thms, [])]) :: notes
         end);

     lthy
     |> primrec_simple0 int plugins nonexhaustive transfer fixes (map snd specs)
     |-> (fn ((names, qualifys), (ts, defs, (jss, simpss))) =>
       Spec_Rules.add Spec_Rules.Equational (ts, flat simpss)
       #> Local_Theory.notes (mk_notes jss names qualifys simpss)
-      #>> (fn notes => (ts, defs, map_filter (fn ("", _) => NONE | (_, thms) => SOME thms) notes)))
+      #-> (fn notes =>
+        plugins code_plugin ? Code.declare_default_eqns (map (rpair true) (maps snd notes))
+        #> pair (ts, defs, map_filter (fn ("", _) => NONE | (_, thms) => SOME thms) notes)))
   end
   handle OLD_PRIMREC () =>
     old_primrec int raw_fixes raw_specs lthy
     |>> (fn (ts, thms) => (ts, [], [thms]));