declare default code equations before custom attributes

--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Sun Aug 31 07:41:41 2025 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Wed Sep 03 08:16:23 2025 +0200
@@ -656,10 +656,9 @@
     |> primrec_simple0 int plugins nonexhaustive transfer fixes (map snd specs)
     |-> (fn {prefix = (names, qualifys), types, result = (ts, defs, (jss, simpss))} =>
       Spec_Rules.add spec_name (Spec_Rules.equational_primrec types) ts (flat simpss)
+      #> plugins code_plugin ? Code.declare_default_eqns (map (rpair true) (flat simpss))
       #> Local_Theory.notes (mk_notes jss names qualifys simpss)
-      #-> (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)))
+      #>> (fn notes => (ts, defs, map_filter (fn ("", _) => NONE | (_, thms) => SOME thms) notes)))
   end
   handle OLD_PRIMREC () =>
     old_primrec int raw_fixes raw_specs lthy

--- a/src/HOL/Tools/Old_Datatype/old_primrec.ML	Sun Aug 31 07:41:41 2025 +0200
+++ b/src/HOL/Tools/Old_Datatype/old_primrec.ML	Wed Sep 03 08:16:23 2025 +0200
@@ -287,11 +287,10 @@
     |> primrec_simple int fixes (map snd spec)
     |-> (fn {prefix, types, result = (ts, simps)} =>
       Spec_Rules.add spec_name (Spec_Rules.equational_primrec types) ts simps
+      #> Code.declare_default_eqns (map (rpair true) simps)
       #> fold_map Local_Theory.note (attr_bindings prefix ~~ map single simps)
       #-> (fn simps' => Local_Theory.note (simp_attr_binding prefix, maps snd simps')
-        #-> (fn (_, simps'') => 
-          Code.declare_default_eqns (map (rpair true) simps'')
-          #> pair {types = types, result = (ts, simps'')})))
+        #>> (fn (_, simps'') => {types = types, result = (ts, simps'')})))
   end;
 
 in