diff -r 079fe4292526 -r c7723cc15de8 src/HOL/Analysis/Measure_Space.thy
--- a/src/HOL/Analysis/Measure_Space.thy	Sun Aug 25 20:54:20 2024 +0200
+++ b/src/HOL/Analysis/Measure_Space.thy	Sun Aug 25 21:10:01 2024 +0200
@@ -1006,6 +1006,9 @@
 syntax
   "_almost_everywhere" :: "pttrn \<Rightarrow> 'a \<Rightarrow> bool \<Rightarrow> bool" ("AE _ in _. _" [0,0,10] 10)
 
+syntax_consts
+  "_almost_everywhere" \<rightleftharpoons> almost_everywhere
+
 translations
   "AE x in M. P" \<rightleftharpoons> "CONST almost_everywhere M (\<lambda>x. P)"
 
@@ -1016,6 +1019,9 @@
   "_set_almost_everywhere" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'a \<Rightarrow> bool \<Rightarrow> bool"
   ("AE _\<in>_ in _./ _" [0,0,0,10] 10)
 
+syntax_consts
+  "_set_almost_everywhere" \<rightleftharpoons> set_almost_everywhere
+
 translations
   "AE x\<in>A in M. P" \<rightleftharpoons> "CONST set_almost_everywhere A M (\<lambda>x. P)"