src/HOL/Tools/BNF/bnf_lfp_size.ML

                 replicate nn [];
           in
             size_gen_o_map_thmss
           end;
 
-      (* Ideally, the "[code]" attribute would be generated only if the "code" plugin is enabled. *)
-      val code_attrs = Code.add_default_eqn_attrib Code.Equation;
-
       val massage_multi_notes =
         maps (fn (thmN, thmss, attrs) =>
           map2 (fn T_name => fn thms =>
               ((Binding.qualify true (Long_Name.base_name T_name) (Binding.name thmN), attrs),
                [(thms, [])]))
             T_names thmss)
         #> filter_out (null o fst o hd o snd);
 
       val notes =
-        [(sizeN, size_thmss, code_attrs :: nitpicksimp_attrs @ simp_attrs),
+        [(sizeN, size_thmss, nitpicksimp_attrs @ simp_attrs),
          (size_genN, size_gen_thmss, []),
          (size_gen_o_mapN, size_gen_o_map_thmss, []),
          (size_neqN, size_neq_thmss, [])]
         |> massage_multi_notes;
 
       val (noted, lthy3) =
         lthy2
         |> Spec_Rules.add Spec_Rules.Equational (size_consts, size_simps)
         |> Spec_Rules.add Spec_Rules.Equational (overloaded_size_consts, overloaded_size_simps)
+        |> Code.declare_default_eqns (map (rpair true) (flat size_thmss))
+          (*Ideally, this would only be issued if the "code" plugin is enabled.*)
         |> Local_Theory.notes notes;
 
       val phi0 = substitute_noted_thm noted;
     in
       lthy3