src/Doc/Datatypes/Datatypes.thy

     no_notation
       Nil ("[]") and
       Cons (infixr "#" 65)
 
     hide_type list
-    hide_const Nil Cons case_list hd tl set map list_all2 rec_list size_list pred_list
+    hide_const Nil Cons case_list hd tl set map list_all2 rec_list size_list list_all
 
     context early
     begin
 (*>*)
     datatype (set: 'a) list =
       null: Nil
     | Cons (hd: 'a) (tl: "'a list")
     for
       map: map
       rel: list_all2
+      pred: list_all
     where
       "tl Nil = Nil"
 
 text \<open>
 \noindent

       null: Nil ("[]")
     | Cons (hd: 'a) (tl: "'a list") (infixr "#" 65)
     for
       map: map
       rel: list_all2
+      pred: list_all
 
 text \<open>
 \noindent
 Incidentally, this is how the traditional syntax can be set up:
 \<close>

 @{term "zs :: ('a \<times> 'b) list"}.
 \<close>
 
     lift_bnf (*<*)(no_warn_wits) (*>*)'a nonempty_list
     proof -
-      fix f and xs :: "'a list"
+      fix f(*<*):: "'a \<Rightarrow> 'c"(*>*) and xs :: "'a list"
       assume "xs \<in> {xs. xs \<noteq> []}"
       then show "map f xs \<in> {xs. xs \<noteq> []}"
         by (cases xs(*<*) rule: list.exhaust(*>*)) auto
     next
       fix zs :: "('a \<times> 'b) list"