diff -r 43df2d59fb98 -r 80b56d9b322f ProgTutorial/Parsing.thy
--- a/ProgTutorial/Parsing.thy	Thu Oct 22 02:03:14 2009 +0200
+++ b/ProgTutorial/Parsing.thy	Thu Oct 22 14:08:23 2009 +0200
@@ -80,7 +80,7 @@
   However, note that these exceptions are private to the parser and cannot be accessed
   by the programmer (for example to handle them).
 
-  In the examples above we use the function @{ML_ind explode in Symbol} in the
+  In the examples above we use the function @{ML_ind explode in Symbol} from the
   structure @{ML_struct Symbol}, instead of the more standard library function
   @{ML_ind explode}, for obtaining an input list for the parser. The reason is
   that @{ML_ind explode} in @{ML_struct Symbol} is aware of character
@@ -148,7 +148,9 @@
 
   The functions @{ML_ind "|--" in Scan} and @{ML_ind "--|" in Scan} work like the sequencing
   function for parsers, except that they discard the item being parsed by the
-  first (respectively second) parser. For example:
+  first (respectively second) parser. That means the item being dropped is the 
+  one that @{ML_ind "|--" in Scan} and @{ML_ind "--|" in Scan} ``point'' away.
+  For example:
   
 @{ML_response [display,gray]
 "let