diff -r 46f59511b7bb -r d97fdabd9e2b src/HOL/TLA/Memory/ProcedureInterface.thy
--- a/src/HOL/TLA/Memory/ProcedureInterface.thy	Fri Sep 20 19:07:10 2024 +0200
+++ b/src/HOL/TLA/Memory/ProcedureInterface.thy	Fri Sep 20 19:51:08 2024 +0200
@@ -41,7 +41,7 @@
   where "slice x i s \<equiv> x s i"
 
 syntax
-  "_slice" :: "[lift, 'a] \<Rightarrow> lift"  ("(_!_)" [70,70] 70)
+  "_slice" :: "[lift, 'a] \<Rightarrow> lift"  (\<open>(_!_)\<close> [70,70] 70)
 translations
   "_slice" \<rightleftharpoons> "CONST slice"
 
@@ -67,8 +67,8 @@
     \<and> (res<ch!p>$ = $v)"
 
 syntax
-  "_Call" :: "['a, 'b, lift] \<Rightarrow> lift"  ("(Call _ _ _)" [90,90,90] 90)
-  "_Return" :: "['a, 'b, lift] \<Rightarrow> lift"  ("(Return _ _ _)" [90,90,90] 90)
+  "_Call" :: "['a, 'b, lift] \<Rightarrow> lift"  (\<open>(Call _ _ _)\<close> [90,90,90] 90)
+  "_Return" :: "['a, 'b, lift] \<Rightarrow> lift"  (\<open>(Return _ _ _)\<close> [90,90,90] 90)
 translations
   "_Call" \<rightleftharpoons> "CONST ACall"
   "_Return" \<rightleftharpoons> "CONST AReturn"