src/Doc/Datatypes/Datatypes.thy

 Polymorphic types are possible, such as the following option type, modeled after
 its homologue from the @{theory Option} theory:
 *}
 
 (*<*)
-    hide_const None Some
+    hide_const None Some map_option
     hide_type option
 (*>*)
     datatype_new 'a option = None | Some 'a
 
 text {*

     no_notation
       Nil ("[]") and
       Cons (infixr "#" 65)
 
     hide_type list
-    hide_const Nil Cons hd tl set map list_all2
+    hide_const Nil Cons hd tl set map list_all2 rec_list size_list
 
     context early begin
 (*>*)
     datatype_new (set: 'a) list (map: map rel: list_all2) =
       null: Nil (defaults tl: Nil)