src/Doc/Datatypes/Datatypes.thy

 (*<*)
     no_translations
       "[x, xs]" == "x # [xs]"
       "[x]" == "x # []"
 
-    no_notation Nil  (\<open>[]\<close>) and Cons  (infixr \<open>#\<close> 65)
-
+    unbundle no list_syntax
     hide_type list
     hide_const Nil Cons case_list hd tl set map list_all2 rec_list size_list list_all
 
     context early
     begin

 text \<open>
 \noindent
 Incidentally, this is how the traditional syntax can be set up:
 \<close>
 (*<*)
-unbundle no list_syntax
+unbundle no list_enumeration_syntax
 (*>*)
     syntax "_list" :: "args \<Rightarrow> 'a list" (\<open>[(_)]\<close>)
 
 text \<open>\blankline\<close>