provide explicit attribute for singleton default equations

--- a/src/Pure/Isar/code.ML	Thu Aug 21 12:09:06 2025 +0200
+++ b/src/Pure/Isar/code.ML	Thu Aug 21 15:13:00 2025 +0200
@@ -41,6 +41,7 @@
   val declare_abstype_global: thm -> theory -> theory
   val declare_default_eqns: (thm * bool) list -> local_theory -> local_theory
   val declare_default_eqns_global: (thm * bool) list -> theory -> theory
+  val singleton_default_equation_attrib: Token.src
   val declare_eqns: (thm * bool) list -> local_theory -> local_theory
   val declare_eqns_global: (thm * bool) list -> theory -> theory
   val declare_abstract_eqn: thm -> local_theory -> local_theory
@@ -1615,9 +1616,12 @@
           add_maybe_abs_eqn_liberal);
   in
     Attrib.setup \<^binding>\<open>code\<close> code_attribute_parser
-        "declare theorems for code generation"
+      "declare theorems for code generation"
   end);
 
+val singleton_default_equation_attrib = Attrib.internal \<^here>
+  (K (code_attribute (fn thm => declare_default_eqns_global [(thm, true)])));
+
 end; (*struct*)
 
 

--- a/src/Pure/Isar/specification.ML	Thu Aug 21 12:09:06 2025 +0200
+++ b/src/Pure/Isar/specification.ML	Thu Aug 21 15:13:00 2025 +0200
@@ -260,11 +260,10 @@
       |> Local_Theory.define_internal ((b, mx), ((Binding.suffix_name "_raw" name, []), rhs));
 
     val ([(def_name, [th])], lthy3) = lthy2
-      |> Local_Theory.notes [((name, atts), [([prove lthy2 raw_th], [])])];
+      |> Local_Theory.notes [((name, Code.singleton_default_equation_attrib :: atts), [([prove lthy2 raw_th], [])])];
 
     val lthy4 = lthy3
-      |> Spec_Rules.add name Spec_Rules.equational [lhs] [th]
-      |> Code.declare_default_eqns [(th, true)];
+      |> Spec_Rules.add name Spec_Rules.equational [lhs] [th];
 
     val lhs' = Morphism.term (Local_Theory.target_morphism lthy4) lhs;