# HG changeset patch
# User blanchet
# Date 1455536836 -3600
# Node ID e1698a9578ea051ba6630bf551517004bf45ffab
# Parent  10332fa721b2d224bab9665e1a0025b7640698c3
document a limitation of 'primcorec'

diff -r 10332fa721b2 -r e1698a9578ea src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Mon Feb 15 12:46:37 2016 +0100
+++ b/src/Doc/Datatypes/Datatypes.thy	Mon Feb 15 12:47:16 2016 +0100
@@ -2090,6 +2090,9 @@
 
 text \<open>
 \noindent
+For technical reasons, @{text "case"}--@{text "of"} is only supported for
+case distinctions on (co)datatypes that provide discriminators and selectors.
+
 Pattern matching is not supported by @{command primcorec}. Fortunately, it is
 easy to generate pattern-maching equations using the @{command simps_of_case}
 command provided by the theory @{file "~~/src/HOL/Library/Simps_Case_Conv.thy"}.
@@ -3462,7 +3465,7 @@
 \setlength{\itemsep}{0pt}
 
 \item
-\emph{Defining mutually (co)recursive (co)datatypes is slow.} Fortunately,
+\emph{Defining mutually (co)recursive (co)datatypes can be slow.} Fortunately,
 it is always possible to recast mutual specifications to nested ones, which are
 processed more efficiently.
 
@@ -3477,6 +3480,11 @@
 \keyw{lemmas} command, is available as an alternative.
 
 \item
+\emph{The \emph{\keyw{primcorec}} command does not allow corecursion under
+@{text "case"}--@{text "of"} for datatypes that are defined without
+discriminators and selectors.
+
+\item
 \emph{There is no way to use an overloaded constant from a syntactic type
 class, such as @{text 0}, as a constructor.}