--- 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)"