diff -r 46f59511b7bb -r d97fdabd9e2b src/HOL/Library/Monad_Syntax.thy
--- a/src/HOL/Library/Monad_Syntax.thy	Fri Sep 20 19:07:10 2024 +0200
+++ b/src/HOL/Library/Monad_Syntax.thy	Fri Sep 20 19:51:08 2024 +0200
@@ -15,10 +15,10 @@
 \<close>
 
 consts
-  bind :: "'a \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> 'd" (infixl "\<bind>" 54)
+  bind :: "'a \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> 'd" (infixl \<open>\<bind>\<close> 54)
 
 notation (ASCII)
-  bind (infixl ">>=" 54)
+  bind (infixl \<open>>>=\<close> 54)
 
 
 abbreviation (do_notation)
@@ -26,25 +26,25 @@
   where "bind_do \<equiv> bind"
 
 notation (output)
-  bind_do (infixl "\<bind>" 54)
+  bind_do (infixl \<open>\<bind>\<close> 54)
 
 notation (ASCII output)
-  bind_do (infixl ">>=" 54)
+  bind_do (infixl \<open>>>=\<close> 54)
 
 
 nonterminal do_binds and do_bind
 syntax
-  "_do_block" :: "do_binds \<Rightarrow> 'a" ("do {//(2  _)//}" [12] 62)
-  "_do_bind"  :: "[pttrn, 'a] \<Rightarrow> do_bind" ("(2_ \<leftarrow>/ _)" 13)
-  "_do_let" :: "[pttrn, 'a] \<Rightarrow> do_bind" ("(2let _ =/ _)" [1000, 13] 13)
-  "_do_then" :: "'a \<Rightarrow> do_bind" ("_" [14] 13)
-  "_do_final" :: "'a \<Rightarrow> do_binds" ("_")
-  "_do_cons" :: "[do_bind, do_binds] \<Rightarrow> do_binds" ("_;//_" [13, 12] 12)
-  "_thenM" :: "['a, 'b] \<Rightarrow> 'c" (infixl "\<then>" 54)
+  "_do_block" :: "do_binds \<Rightarrow> 'a" (\<open>do {//(2  _)//}\<close> [12] 62)
+  "_do_bind"  :: "[pttrn, 'a] \<Rightarrow> do_bind" (\<open>(2_ \<leftarrow>/ _)\<close> 13)
+  "_do_let" :: "[pttrn, 'a] \<Rightarrow> do_bind" (\<open>(2let _ =/ _)\<close> [1000, 13] 13)
+  "_do_then" :: "'a \<Rightarrow> do_bind" (\<open>_\<close> [14] 13)
+  "_do_final" :: "'a \<Rightarrow> do_binds" (\<open>_\<close>)
+  "_do_cons" :: "[do_bind, do_binds] \<Rightarrow> do_binds" (\<open>_;//_\<close> [13, 12] 12)
+  "_thenM" :: "['a, 'b] \<Rightarrow> 'c" (infixl \<open>\<then>\<close> 54)
 
 syntax (ASCII)
-  "_do_bind" :: "[pttrn, 'a] \<Rightarrow> do_bind" ("(2_ <-/ _)" 13)
-  "_thenM" :: "['a, 'b] \<Rightarrow> 'c" (infixl ">>" 54)
+  "_do_bind" :: "[pttrn, 'a] \<Rightarrow> do_bind" (\<open>(2_ <-/ _)\<close> 13)
+  "_thenM" :: "['a, 'b] \<Rightarrow> 'c" (infixl \<open>>>\<close> 54)
 
 syntax_consts
   "_do_block" "_do_cons" "_do_bind" "_do_then" \<rightleftharpoons> bind and