--- a/ProgTutorial/Parsing.thy	Thu Nov 19 20:00:10 2009 +0100
+++ b/ProgTutorial/Parsing.thy	Thu Nov 19 20:23:15 2009 +0100
@@ -374,9 +374,11 @@
 
   \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 datastructure. 
-  We assume the trees are represented by the datatype:
+  Be aware of recursive parsers. Suppose you want to read strings separated by
+  commas and by parentheses into a tree datastructure; for example, generating
+  the tree corresponding to the string @{text [quotes] "(A, A), (A, A)"} where
+  the @{text "A"}s will be the leaves.  We assume the trees are represented by the
+  datatype:
 *}
 
 ML{*datatype tree = 
@@ -390,13 +392,21 @@
 *}
 
 ML{*fun parse_basic s = 
-  $$ s >> Lf 
-  || $$ "(" |-- parse_tree s --| $$ ")"  
+  $$ s >> Lf || $$ "(" |-- parse_tree s --| $$ ")"  
+
 and parse_tree s = 
-  parse_basic s --| $$ "," -- parse_tree s >> Br 
-  || parse_basic s*}
+  parse_basic s --| $$ "," -- parse_tree s >> Br || parse_basic s*}
 
 text {*
+  This parser corrsponds to the grammar:
+
+  \begin{center}
+  \begin{tabular}{lcl}
+  @{text "<Basic>"}  & @{text "::="} & @{text "<String> | (<Tree>)"}\\
+  @{text "<Tree>"}   & @{text "::="} & @{text "<Basic>, <Tree> | <Basic>"}\\
+  \end{tabular}
+  \end{center}
+
   The parameter @{text "s"} is the string over which the tree is parsed. The
   parser @{ML parse_basic} reads either a leaf or a tree enclosed in
   parentheses. The parser @{ML parse_tree} reads either a pair of trees
@@ -412,15 +422,15 @@
   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.
+  string as an explicit argument. So the parser above should be implemented
+  as follows.
 *}
 
 ML{*fun parse_basic s xs = 
-  ($$ s >> Lf 
-   || $$ "(" |-- parse_tree s --| $$ ")") xs 
+  ($$ s >> Lf || $$ "(" |-- parse_tree s --| $$ ")") xs 
+
 and parse_tree s xs = 
-  (parse_basic s --| $$ "," -- parse_tree s >> Br 
-   || parse_basic s) xs*}
+  (parse_basic s --| $$ "," -- parse_tree s >> Br || parse_basic s) xs*}
 
 text {*
   While the type of the parser is unchanged by the addition, its behaviour