diff -r 20235f0512e2 -r 919186869943 src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Tue Oct 21 17:23:12 2014 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy	Tue Oct 21 17:23:13 2014 +0200
@@ -1855,6 +1855,9 @@
 @{thm llist.corec_sel(1)[no_vars]} \\
 @{thm llist.corec_sel(2)[no_vars]}
 
+\item[@{text "t."}\hthm{map_o_corec}\rm:] ~ \\
+@{thm llist.map_o_corec[no_vars]}
+
 \item[@{text "t."}\hthm{corec_transfer}\rm:] ~ \\
 @{thm llist.corec_transfer[no_vars]}