document the new 'nonexhaustive' option (cf. 52e8f110fec3)

--- a/src/Doc/Datatypes/Datatypes.thy	Fri Mar 14 09:56:06 2014 +0100
+++ b/src/Doc/Datatypes/Datatypes.thy	Fri Mar 14 10:08:33 2014 +0100
@@ -1355,7 +1355,7 @@
   \label{ssec:primrec-command-syntax} *}
 
 
-subsubsection {* \keyw{primrec\_new}
+subsubsection {* \keyw{primrec}
   \label{sssec:primrec-new} *}
 
 text {*
@@ -1364,7 +1364,10 @@
 \end{matharray}
 
 @{rail \<open>
-  @@{command primrec} target? fixes \<newline> @'where' (@{syntax pr_equation} + '|')
+  @@{command primrec} target? @{syntax pr_option}? fixes \<newline>
+  @'where' (@{syntax pr_equation} + '|')
+  ;
+  @{syntax_def pr_option}: '(' 'nonexhaustive' ')'
   ;
   @{syntax_def pr_equation}: thmdecl? prop
 \<close>}
@@ -1380,6 +1383,17 @@
 \synt{thmdecl} denotes an optional name for the formula that follows, and
 \synt{prop} denotes a HOL proposition \cite{isabelle-isar-ref}.
 
+The optional target is potentially followed by a recursion-specific option:
+
+\begin{itemize}
+\setlength{\itemsep}{0pt}
+
+\item
+The @{text "nonexhaustive"} option indicates that the functions are not
+necessarily specified for all constructors. It can be used to suppress the
+warning that is normally emitted when some constructors are missing.
+\end{itemize}
+
 %%% TODO: elaborate on format of the equations
 %%% TODO: elaborate on mutual and nested-to-mutual
 *}