# HG changeset patch
# User wenzelm
# Date 1756381792 -7200
# Node ID 08ad23c75b88c4fe53a59c8df121b71d714053f2
# Parent  f8f82da1e560b48b03a45eb5462697ae8ae86290
tuned whitespace;

diff -r f8f82da1e560 -r 08ad23c75b88 src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Wed Aug 27 20:42:15 2025 +0200
+++ b/src/Pure/Isar/specification.ML	Thu Aug 28 13:49:52 2025 +0200
@@ -260,7 +260,8 @@
       |> Local_Theory.define_internal ((b, mx), ((Binding.suffix_name "_raw" name, []), rhs));
 
     val ([(def_name, [th])], lthy3) = lthy2
-      |> Local_Theory.notes [((name, Code.singleton_default_equation_attrib :: 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];