src/Doc/Datatypes/Datatypes.thy
changeset 56995 61855ade6c7e
parent 56992 d0e5225601d3
child 57047 90d4db566e12
--- a/src/Doc/Datatypes/Datatypes.thy	Mon May 19 13:44:13 2014 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy	Mon May 19 13:53:58 2014 +0200
@@ -194,7 +194,7 @@
 *}
 
 (*<*)
-    hide_const None Some
+    hide_const None Some map_option
     hide_type option
 (*>*)
     datatype_new 'a option = None | Some 'a
@@ -367,7 +367,7 @@
       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
 (*>*)