--- a/src/HOL/HOLCF/FOCUS/Buffer.thy	Fri Sep 20 19:07:10 2024 +0200
+++ b/src/HOL/HOLCF/FOCUS/Buffer.thy	Fri Sep 20 19:51:08 2024 +0200
@@ -26,10 +26,10 @@
 typedecl D
 
 datatype
-  M     = Md D | Mreq ("\<bullet>")
+  M     = Md D | Mreq (\<open>\<bullet>\<close>)
 
 datatype
-  State = Sd D | Snil ("\<currency>")
+  State = Sd D | Snil (\<open>\<currency>\<close>)
 
 type_synonym
   SPF11         = "M fstream \<rightarrow> D fstream"