diff -r d90869a85f60 -r 2b949a3bfaac src/Doc/Tutorial/ToyList/ToyList.thy
--- a/src/Doc/Tutorial/ToyList/ToyList.thy	Tue Oct 08 23:31:06 2024 +0200
+++ b/src/Doc/Tutorial/ToyList/ToyList.thy	Wed Oct 09 13:06:55 2024 +0200
@@ -9,7 +9,8 @@
 the concrete syntax and name space of theory \<^theory>\<open>Main\<close> as follows.
 \<close>
 
-no_notation Nil  ("[]") and Cons  (infixr "#" 65) and append  (infixr "@" 65)
+unbundle no list_syntax
+no_notation append  (infixr "@" 65)
 hide_type list
 hide_const rev