diff -r 46f59511b7bb -r d97fdabd9e2b src/HOL/HOLCF/IOA/Sequence.thy
--- a/src/HOL/HOLCF/IOA/Sequence.thy	Fri Sep 20 19:07:10 2024 +0200
+++ b/src/HOL/HOLCF/IOA/Sequence.thy	Fri Sep 20 19:51:08 2024 +0200
@@ -63,7 +63,7 @@
               UU \<Rightarrow> UU
             | Def y \<Rightarrow> (if P y then x ## (h \<cdot> xs) else h \<cdot> xs))))"
 
-abbreviation Consq_syn  ("(_/\<leadsto>_)" [66, 65] 65)
+abbreviation Consq_syn  (\<open>(_/\<leadsto>_)\<close> [66, 65] 65)
   where "a \<leadsto> s \<equiv> Consq a \<cdot> s"
 
 
@@ -71,10 +71,10 @@
 
 nonterminal llist_args
 syntax
-  "" :: "'a \<Rightarrow> llist_args"  ("_")
-  "_list_args" :: "'a \<Rightarrow> llist_args \<Rightarrow> llist_args"  ("_,/ _")
-  "_totlist" :: "llist_args \<Rightarrow> 'a Seq"  ("[(_)!]")
-  "_partlist" :: "llist_args \<Rightarrow> 'a Seq"  ("[(_)?]")
+  "" :: "'a \<Rightarrow> llist_args"  (\<open>_\<close>)
+  "_list_args" :: "'a \<Rightarrow> llist_args \<Rightarrow> llist_args"  (\<open>_,/ _\<close>)
+  "_totlist" :: "llist_args \<Rightarrow> 'a Seq"  (\<open>[(_)!]\<close>)
+  "_partlist" :: "llist_args \<Rightarrow> 'a Seq"  (\<open>[(_)?]\<close>)
 syntax_consts
   "_totlist" "_partlist" \<rightleftharpoons> Consq
 translations