src/Doc/Datatypes/Datatypes.thy

 
 \item[@{text "t."}\hthm{case} @{text "[simp, code]"}\rm:] ~ \\
 @{thm list.case(1)[no_vars]} \\
 @{thm list.case(2)[no_vars]}
 
-\item[@{text "t."}\hthm{case\_cong}\rm:] ~ \\
+\item[@{text "t."}\hthm{case\_cong} @{text "[fundef_cong]"}\rm:] ~ \\
 @{thm list.case_cong[no_vars]}
 
 \item[@{text "t."}\hthm{weak\_case\_cong} @{text "[cong]"}\rm:] ~ \\
 @{thm list.weak_case_cong[no_vars]}
 

 
 % options: no_discs_sels no_code rep_compat
 
 \noindent
 Section~\ref{ssec:datatype-generated-theorems} lists the generated theorems.
+For technical reasons, the @{text "[fundef_cong]"} attribute is not set on the
+generated @{text case_cong} theorem. It can be added manually using
+\keyw{declare}.
 *}
 
 
 (*
 section {* Standard ML Interface