diff -r 46f59511b7bb -r d97fdabd9e2b src/HOL/HOLCF/Ssum.thy
--- a/src/HOL/HOLCF/Ssum.thy	Fri Sep 20 19:07:10 2024 +0200
+++ b/src/HOL/HOLCF/Ssum.thy	Fri Sep 20 19:51:08 2024 +0200
@@ -19,14 +19,14 @@
     (fst p = TT \<and> fst (snd p) \<noteq> \<bottom> \<and> snd (snd p) = \<bottom>) \<or>
     (fst p = FF \<and> fst (snd p) = \<bottom> \<and> snd (snd p) \<noteq> \<bottom>)}"
 
-pcpodef ('a, 'b) ssum  ("(_ \<oplus>/ _)" [21, 20] 20) = "ssum :: (tr \<times> 'a \<times> 'b) set"
+pcpodef ('a, 'b) ssum  (\<open>(_ \<oplus>/ _)\<close> [21, 20] 20) = "ssum :: (tr \<times> 'a \<times> 'b) set"
   by (simp_all add: ssum_def)
 
 instance ssum :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin
   by (rule typedef_chfin [OF type_definition_ssum below_ssum_def])
 
 type_notation (ASCII)
-  ssum  (infixr "++" 10)
+  ssum  (infixr \<open>++\<close> 10)
 
 
 subsection \<open>Definitions of constructors\<close>