diff -r e2cdcb656b24 -r ba4d3d4a1e0f src/Pure/Isar/specification.ML
--- 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;