1.1 --- a/src/Doc/Datatypes/Datatypes.thy	Wed Jul 02 17:01:49 2014 +0200
     1.2 +++ b/src/Doc/Datatypes/Datatypes.thy	Wed Jul 02 17:01:51 2014 +0200
     1.3 @@ -1766,6 +1766,9 @@
     1.4  @{thm llist.corec(1)[no_vars]} \\
     1.5  @{thm llist.corec(2)[no_vars]}
     1.6  
     1.7 +\item[@{text "t."}\hthm{corec\_code} @{text "[code]"}\rm:] ~ \\
     1.8 +@{thm llist.corec_code[no_vars]}
     1.9 +
    1.10  \item[@{text "t."}\hthm{disc\_corec}\rm:] ~ \\
    1.11  @{thm llist.disc_corec(1)[no_vars]} \\
    1.12  @{thm llist.disc_corec(2)[no_vars]}