--- 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.