1.1 --- a/src/Doc/Datatypes/Datatypes.thy	Wed Feb 12 08:35:56 2014 +0100
     1.2 +++ b/src/Doc/Datatypes/Datatypes.thy	Wed Feb 12 08:35:56 2014 +0100
     1.3 @@ -771,7 +771,7 @@
     1.4  @{thm list.case(1)[no_vars]} \\
     1.5  @{thm list.case(2)[no_vars]}
     1.6  
     1.7 -\item[@{text "t."}\hthm{case\_cong}\rm:] ~ \\
     1.8 +\item[@{text "t."}\hthm{case\_cong} @{text "[fundef_cong]"}\rm:] ~ \\
     1.9  @{thm list.case_cong[no_vars]}
    1.10  
    1.11  \item[@{text "t."}\hthm{weak\_case\_cong} @{text "[cong]"}\rm:] ~ \\
    1.12 @@ -2605,6 +2605,9 @@
    1.13  
    1.14  \noindent
    1.15  Section~\ref{ssec:datatype-generated-theorems} lists the generated theorems.
    1.16 +For technical reasons, the @{text "[fundef_cong]"} attribute is not set on the
    1.17 +generated @{text case_cong} theorem. It can be added manually using
    1.18 +\keyw{declare}.
    1.19  *}
    1.20  
    1.21