diff -r 46f59511b7bb -r d97fdabd9e2b src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Fri Sep 20 19:07:10 2024 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy	Fri Sep 20 19:51:08 2024 +0200
@@ -361,8 +361,8 @@
       "[x]" == "x # []"
 
     no_notation
-      Nil ("[]") and
-      Cons (infixr "#" 65)
+      Nil (\<open>[]\<close>) and
+      Cons (infixr \<open>#\<close> 65)
 
     hide_type list
     hide_const Nil Cons case_list hd tl set map list_all2 rec_list size_list list_all
@@ -436,13 +436,13 @@
 (*<*)
     end
 (*>*)
-    datatype ('a, 'b) prod (infixr "*" 20) = Pair 'a 'b
+    datatype ('a, 'b) prod (infixr \<open>*\<close> 20) = Pair 'a 'b
 
 text \<open>\blankline\<close>
 
     datatype (set: 'a) list =
-      null: Nil ("[]")
-    | Cons (hd: 'a) (tl: "'a list") (infixr "#" 65)
+      null: Nil (\<open>[]\<close>)
+    | Cons (hd: 'a) (tl: "'a list") (infixr \<open>#\<close> 65)
     for
       map: map
       rel: list_all2
@@ -453,7 +453,7 @@
 Incidentally, this is how the traditional syntax can be set up:
 \<close>
 
-    syntax "_list" :: "list_args \<Rightarrow> 'a list" ("[(_)]")
+    syntax "_list" :: "list_args \<Rightarrow> 'a list" (\<open>[(_)]\<close>)
 
 text \<open>\blankline\<close>