diff -r ff2a637a449e -r fc5066122e68 src/Pure/Examples/Higher_Order_Logic.thy
--- a/src/Pure/Examples/Higher_Order_Logic.thy	Fri Oct 18 11:44:05 2024 +0200
+++ b/src/Pure/Examples/Higher_Order_Logic.thy	Fri Oct 18 14:20:09 2024 +0200
@@ -401,7 +401,7 @@
 axiomatization Eps :: "('a \<Rightarrow> o) \<Rightarrow> 'a"
   where someI: "P x \<Longrightarrow> P (Eps P)"
 
-syntax "_Eps" :: "pttrn \<Rightarrow> o \<Rightarrow> 'a"  (\<open>(3SOME _./ _)\<close> [0, 10] 10)
+syntax "_Eps" :: "pttrn \<Rightarrow> o \<Rightarrow> 'a"  (\<open>(\<open>indent=3 notation=\<open>binder SOME\<close>\<close>SOME _./ _)\<close> [0, 10] 10)
 syntax_consts "_Eps" \<rightleftharpoons> Eps
 translations "SOME x. P" \<rightleftharpoons> "CONST Eps (\<lambda>x. P)"