--- a/CookBook/Parsing.thy	Mon Feb 23 17:08:15 2009 +0000
+++ b/CookBook/Parsing.thy	Tue Feb 24 01:30:15 2009 +0000
@@ -204,11 +204,11 @@
 *}
 
 ML{*fun p_followed_by_q p q r =
-  let 
-     val err_msg = (fn _ => p ^ " is not followed by " ^ q)
-  in
-    ($$ p -- (!! err_msg ($$ q))) || ($$ r -- $$ r)
-  end *}
+let 
+  val err_msg = (fn _ => p ^ " is not followed by " ^ q)
+in
+  ($$ p -- (!! err_msg ($$ q))) || ($$ r -- $$ r)
+end *}
 
 
 text {*
@@ -348,7 +348,7 @@
 
 text {*
   Most of the time, however, Isabelle developers have to deal with parsing
-  tokens, not strings.  These token parsers will have the type
+  tokens, not strings.  These token parsers will have the type:
 *}
   
 ML{*type 'a parser = OuterLex.token list -> 'a * OuterLex.token list*}
@@ -727,7 +727,7 @@
   The function @{ML opt_thm_name in SpecParse} is the ``optional'' variant of
   @{ML thm_name in SpecParse}. Theorem names can contain attributes. The name 
   has to end with @{text [quotes] ":"}---see the argument of 
-  @{ML SpecParse.opt_thm_name} in Line 9.
+  the function @{ML SpecParse.opt_thm_name} in Line 9.
 
   \begin{readmore}
   Attributes and arguments are implemented in the files @{ML_file "Pure/Isar/attrib.ML"}