--- a/ProgTutorial/Parsing.thy	Tue Nov 17 20:36:18 2009 +0100
+++ b/ProgTutorial/Parsing.thy	Tue Nov 17 23:59:19 2009 +0100
@@ -375,8 +375,8 @@
   \footnote{\bf FIXME: In which situations is @{text "lift"} useful? Give examples.} 
 
   Be aware of recursive parsers. Suppose you want to read strings
-  separated by commas and by parentheses into a tree. We assume 
-  the trees are represented by the datatype:
+  separated by commas and by parentheses into a tree datastructure. 
+  We assume the trees are represented by the datatype:
 *}
 
 ML{*datatype tree = 
@@ -409,7 +409,7 @@
   "*** Exception- TOPLEVEL_ERROR raised"}
 
   raises an exception indicating that the stack limit is reached. Such
-  looping parser are not useful at all, because of ML's strict evaluation of
+  looping parser are not useful, because of ML's strict evaluation of
   arguments. Therefore we need to delay the execution of the
   parser until an input is given. This can be done by adding the parsed
   string as an explicit argument.