diff -r 46f59511b7bb -r d97fdabd9e2b src/HOL/Analysis/Sigma_Algebra.thy
--- a/src/HOL/Analysis/Sigma_Algebra.thy	Fri Sep 20 19:07:10 2024 +0200
+++ b/src/HOL/Analysis/Sigma_Algebra.thy	Fri Sep 20 19:51:08 2024 +0200
@@ -1759,7 +1759,7 @@
 subsubsection \<open>Measurable functions\<close>
 
 definition\<^marker>\<open>tag important\<close> measurable :: "'a measure \<Rightarrow> 'b measure \<Rightarrow> ('a \<Rightarrow> 'b) set"
-  (infixr "\<rightarrow>\<^sub>M" 60) where
+  (infixr \<open>\<rightarrow>\<^sub>M\<close> 60) where
 "measurable A B = {f \<in> space A \<rightarrow> space B. \<forall>y \<in> sets B. f -` y \<inter> space A \<in> sets A}"
 
 lemma measurableI: