--- a/doc-src/Logics/HOL.tex Fri Apr 18 16:54:52 1997 +0200
+++ b/doc-src/Logics/HOL.tex Fri Apr 18 17:33:26 1997 +0200
@@ -952,6 +952,7 @@
\S\ref{sec:HOL:datatype}.
\subsection{Product and sum types}\index{*"* type}\index{*"+ type}
+\label{subsec:prod-sum}
\begin{figure}[htbp]
\begin{constants}
@@ -1576,10 +1577,12 @@
\mid & C_m~x_{m1}~\dots~x_{mk_m} & \To & e_m
\end{array}
\]
+where the $x_{ij}$ are either identifiers or nested tuple patterns as in
+\S\ref{subsec:prod-sum}.
\begin{warn}
In contrast to \ML, {\em all} constructors must be present, their order is
-fixed, and nested patterns are not supported. Violating this restriction
-results in strange error messages.
+fixed, and nested patterns are not supported (with the exception of tuples).
+Violating this restriction results in strange error messages.
\end{warn}
\underscoreoff