--- 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;