--- a/src/HOL/Library/Quotient_Syntax.thy	Fri Sep 20 19:07:10 2024 +0200
+++ b/src/HOL/Library/Quotient_Syntax.thy	Fri Sep 20 19:51:08 2024 +0200
@@ -9,8 +9,8 @@
 begin
 
 notation
-  rel_conj (infixr "OOO" 75) and
-  map_fun (infixr "--->" 55) and
-  rel_fun (infixr "===>" 55)
+  rel_conj (infixr \<open>OOO\<close> 75) and
+  map_fun (infixr \<open>--->\<close> 55) and
+  rel_fun (infixr \<open>===>\<close> 55)
 
 end