diff -r 46f59511b7bb -r d97fdabd9e2b src/HOL/Probability/Fin_Map.thy
--- a/src/HOL/Probability/Fin_Map.thy	Fri Sep 20 19:07:10 2024 +0200
+++ b/src/HOL/Probability/Fin_Map.thy	Fri Sep 20 19:51:08 2024 +0200
@@ -13,7 +13,7 @@
   stay close to the developments of (finite) products \<^const>\<open>Pi\<^sub>E\<close> and their sigma-algebra
   \<^const>\<open>Pi\<^sub>M\<close>.\<close>
 
-type_notation fmap ("(_ \<Rightarrow>\<^sub>F /_)" [22, 21] 21)
+type_notation fmap (\<open>(_ \<Rightarrow>\<^sub>F /_)\<close> [22, 21] 21)
 
 unbundle fmap.lifting
 
@@ -25,7 +25,7 @@
 lemma finite_domain[simp, intro]: "finite (domain P)"
   by transfer simp
 
-lift_definition proj :: "('i \<Rightarrow>\<^sub>F 'a) \<Rightarrow> 'i \<Rightarrow> 'a" ("'((_)')\<^sub>F" [0] 1000) is
+lift_definition proj :: "('i \<Rightarrow>\<^sub>F 'a) \<Rightarrow> 'i \<Rightarrow> 'a" (\<open>'((_)')\<^sub>F\<close> [0] 1000) is
   "\<lambda>f x. if x \<in> dom f then the (f x) else undefined" .
 
 declare [[coercion proj]]
@@ -89,7 +89,7 @@
   "Pi' I A = { P. domain P = I \<and> (\<forall>i. i \<in> I \<longrightarrow> (P)\<^sub>F i \<in> A i) } "
 
 syntax
-  "_Pi'" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set"  ("(3\<Pi>'' _\<in>_./ _)"   10)
+  "_Pi'" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set"  (\<open>(3\<Pi>'' _\<in>_./ _)\<close>   10)
 syntax_consts
   "_Pi'" == Pi'
 translations
@@ -636,7 +636,7 @@
   "Pi\<^sub>F I M \<equiv> PiF I M"
 
 syntax
-  "_PiF" :: "pttrn \<Rightarrow> 'i set \<Rightarrow> 'a measure \<Rightarrow> ('i => 'a) measure"  ("(3\<Pi>\<^sub>F _\<in>_./ _)"  10)
+  "_PiF" :: "pttrn \<Rightarrow> 'i set \<Rightarrow> 'a measure \<Rightarrow> ('i => 'a) measure"  (\<open>(3\<Pi>\<^sub>F _\<in>_./ _)\<close>  10)
 syntax_consts
   "_PiF" == PiF
 translations