diff -r 46f59511b7bb -r d97fdabd9e2b src/HOL/Analysis/Measure_Space.thy
--- a/src/HOL/Analysis/Measure_Space.thy	Fri Sep 20 19:07:10 2024 +0200
+++ b/src/HOL/Analysis/Measure_Space.thy	Fri Sep 20 19:51:08 2024 +0200
@@ -1004,7 +1004,7 @@
   "almost_everywhere M P \<equiv> eventually P (ae_filter M)"
 
 syntax
-  "_almost_everywhere" :: "pttrn \<Rightarrow> 'a \<Rightarrow> bool \<Rightarrow> bool" ("AE _ in _. _" [0,0,10] 10)
+  "_almost_everywhere" :: "pttrn \<Rightarrow> 'a \<Rightarrow> bool \<Rightarrow> bool" (\<open>AE _ in _. _\<close> [0,0,10] 10)
 
 syntax_consts
   "_almost_everywhere" \<rightleftharpoons> almost_everywhere
@@ -1017,7 +1017,7 @@
 
 syntax
   "_set_almost_everywhere" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'a \<Rightarrow> bool \<Rightarrow> bool"
-  ("AE _\<in>_ in _./ _" [0,0,0,10] 10)
+  (\<open>AE _\<in>_ in _./ _\<close> [0,0,0,10] 10)
 
 syntax_consts
   "_set_almost_everywhere" \<rightleftharpoons> set_almost_everywhere