--- a/ProgTutorial/Parsing.thy Sat May 09 18:50:01 2009 +0200
+++ b/ProgTutorial/Parsing.thy Sun May 17 16:22:27 2009 +0200
@@ -1333,7 +1333,7 @@
Input text is split up into tokens, and the input source type for many parsing
functions is \texttt{token list}.
- The data type definition (which is not published in the signature) is
+ The datatype definition (which is not published in the signature) is
\begin{verbatim}
datatype token = Token of Position.T * (token_kind * string);
\end{verbatim}
@@ -1518,7 +1518,7 @@
text {*
The source file is \texttt{src/Pure/Isar/args.ML}.
- The primary type of this structure is the \texttt{src} data type;
+ The primary type of this structure is the \texttt{src} datatype;
the single constructors not published in the signature, but
\texttt{Args.src} and \texttt{Args.dest\_src}
are in fact the constructor and destructor functions.