diff -r 7638776e0977 -r 2cc651d3ce8e src/Doc/Tutorial/ToyList/ToyList.thy
--- a/src/Doc/Tutorial/ToyList/ToyList.thy	Fri Sep 27 22:44:30 2024 +0200
+++ b/src/Doc/Tutorial/ToyList/ToyList.thy	Fri Sep 27 23:47:45 2024 +0200
@@ -9,12 +9,12 @@
 the concrete syntax and name space of theory \<^theory>\<open>Main\<close> as follows.
 \<close>
 
-no_notation Nil (\<open>[]\<close>) and Cons (infixr \<open>#\<close> 65) and append (infixr \<open>@\<close> 65)
+no_notation Nil ("[]") and Cons (infixr "#" 65) and append (infixr "@" 65)
 hide_type list
 hide_const rev
 
-datatype 'a list = Nil                          (\<open>[]\<close>)
-                 | Cons 'a "'a list"            (infixr \<open>#\<close> 65)
+datatype 'a list = Nil                          ("[]")
+                 | Cons 'a "'a list"            (infixr "#" 65)
 
 text\<open>\noindent
 The datatype\index{datatype@\isacommand {datatype} (command)}
@@ -47,7 +47,7 @@
 in this order, because Isabelle insists on definition before use:
 \<close>
 
-primrec app :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" (infixr \<open>@\<close> 65) where
+primrec app :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" (infixr "@" 65) where
 "[] @ ys       = ys" |
 "(x # xs) @ ys = x # (xs @ ys)"