diff -r 4daf913fdbe1 -r 609f9ef73494 CookBook/Parsing.thy
--- a/CookBook/Parsing.thy	Thu Oct 30 13:36:51 2008 +0100
+++ b/CookBook/Parsing.thy	Sat Nov 01 15:20:36 2008 +0100
@@ -213,9 +213,7 @@
   Note that @{ML "Scan.repeat"} stores the parsed items in a list. The function
   @{ML "Scan.repeat1"} is similar, but requires that the parser @{ML_text "p"} 
   succeeds at least once.
-*}
- 
-text {* 
+
   After parsing succeeded, one nearly always wants to apply a function on the parsed 
   items. This is done using the function @{ML_open "(p >> f)" for p f} which runs 
   first the parser @{ML_text p} and upon successful completion applies the 
@@ -273,14 +271,16 @@
 
   produces three tokens where the first and the last are identifiers, since 
   @{ML_text [quotes] "hello"} and @{ML_text [quotes] "world"} do not match 
-  any other category. The second indicates a space. If we parse
+  any other category. The second indicates a space. Many parsing functions 
+  later on will require spaces, comments and the like to have been filtered out.
+  If we parse
 
 @{ML_response [display] "OuterSyntax.scan Position.none \"inductive|for\"" 
 "[OuterLex.Token (\<dots>,(OuterLex.Command, \"inductive\"),\<dots>), 
  OuterLex.Token (\<dots>,(OuterLex.Keyword, \"|\"),\<dots>), 
  OuterLex.Token (\<dots>,(OuterLex.Keyword, \"for\"),\<dots>)]"}
 
-  we obtain a list of command and keyword tokens.
+  we obtain a list consiting of only command and keyword tokens.
   If you want to see which keywords and commands are currently known, use
   the following (you might have to adjust the @{ML print_depth} in order to
   see the complete list):
@@ -305,7 +305,6 @@
 "((\"where\",\<dots>),(\"|\",\<dots>))"}
 
   Like before, we can sequentially connect parsers with @{ML "(op --)"}. For example 
-  follows
 
 @{ML_response [display]
 "let 
@@ -316,7 +315,7 @@
 "((\"|\",\"in\"),[])"}
 
   The parser @{ML_open "OuterParse.enum s p" for s p} parses a possibly empty 
-  list of items recognized by the parser @{ML_text p}, where the items are 
+  list of items recognised by the parser @{ML_text p}, where the items are 
   separated by @{ML_text s}. For example
 
 @{ML_response [display]
@@ -329,7 +328,7 @@
 
   Note that we had to add a @{ML_text [quotes] "\\n"} at the end of the parsed
   string, otherwise the parser would have consumed all tokens and then failed with
-  the exception @{ML_text "FAIL"}. @{ML "OuterParse.enum1"} works similarly, 
+  the exception @{ML_text "MORE"}. @{ML "OuterParse.enum1"} works similarly, 
   except that the parsed list must be non-empty.
 
 *}