--- a/CookBook/Parsing.thy	Thu Feb 19 01:09:16 2009 +0000
+++ b/CookBook/Parsing.thy	Thu Feb 19 14:44:53 2009 +0000
@@ -527,7 +527,7 @@
   in which the @{text [quotes] "\\n"} causes the second token to be in 
   line 8.
 
-  Now by using the parser @{ML OuterParse.position} you can decode the positional
+  By using the parser @{ML OuterParse.position} you can decode the positional
   information and return it as part of the parsed input. For example
 
 @{ML_response_fake [display,gray]
@@ -563,7 +563,7 @@
   The function @{ML OuterParse.prop} is similar, except that it gives a different
   error message, when parsing fails. Looking closer at the result string you will
   have noticed that the parser not just returns the parsed string, but also some 
-  encoded positional information. You can see this better if you replace 
+  encoded information. You can see this better if you replace 
   @{ML Position.none} by @{ML "(Position.line 42)"}, say.
 
 @{ML_response [display,gray]
@@ -574,7 +574,7 @@
 end"
 "(\"\\^E\\^Ftoken\\^Fline=42\\^Fend_line=42\\^Efoo\\^E\\^F\\^E\", [])"}
   
-  The positional information is stored so that code called later will be
+  The positional information is stored so that code called later on will be
   able to give more precise error messages. 
 
 *}
@@ -606,18 +606,21 @@
 *}
 
 ML %linenosgray{*val spec_parser = 
-    OuterParse.opt_target --
-    OuterParse.fixes -- 
-    OuterParse.for_fixes --
-    Scan.optional 
-      (OuterParse.$$$ "where" |--
-         OuterParse.!!! 
-           (OuterParse.enum1 "|" 
-              (SpecParse.opt_thm_name ":" -- OuterParse.prop))) []*}
+     OuterParse.opt_target --
+     OuterParse.fixes -- 
+     OuterParse.for_fixes --
+     Scan.optional 
+       (OuterParse.$$$ "where" |--
+          OuterParse.!!! 
+            (OuterParse.enum1 "|" 
+               (SpecParse.opt_thm_name ":" -- OuterParse.prop))) []*}
 
 text {*
-  Note that the parser does not parse the ketword \simpleinductive. This 
-  will be done by the infrastructure that will eventually call this parser.
+  Note that the parser does not parse the keyword \simpleinductive, even if it is
+  meant to process definitions as shown above. The parser of the keyword 
+  will be given by the infrastructure that will eventually calls @{ML spec_parser}.
+  
+
   To see what the parser returns, let us parse the string corresponding to the 
   definition of @{term even} and @{term odd}:
 
@@ -638,9 +641,10 @@
       ((oddS,\<dots>), \"\\^E\\^Ftoken\\^Eeven n \<Longrightarrow> odd (Suc n)\\^E\\^F\\^E\")]), [])"}
 
   As can be seen, the result is a ``nested'' four-tuple consisting of an 
-  optional locale; a list of variables with optional type-annotation and  
-  syntax-annotation; a list of for-fixes (fixed variables); and a list of rules 
-  where each rule has optionally a name and an attribute.
+  optional locale (in this case @{ML NONE}); a list of variables with optional 
+  type-annotation and syntax-annotation; a list of for-fixes (fixed variables; in this
+  case there are none); and a list of rules where every rule has optionally a name and 
+  an attribute.
 
   In Line 2 of the parser, the function @{ML OuterParse.opt_target} reads a target 
   in order to indicate a locale in which the specification is made. For example
@@ -648,8 +652,8 @@
 @{ML_response [display,gray]
 "parse OuterParse.opt_target (filtered_input \"(in test)\")" "(SOME \"test\",[])"}
   
-  returns the locale @{text [quotes] "test"}; if no target is given' like in  the
-  casde of @{text "even"} and @{text "odd"}, the function returns @{ML NONE}.
+  returns the locale @{text [quotes] "test"}; if no target is given, like in  the
+  case of @{text "even"} and @{text "odd"}, the function returns @{ML NONE}.
 
   The function @{ML OuterParse.fixes} in Line 3 reads an \isacommand{and}-separated 
   list of variables that can include optional type annotations and syntax translations. 
@@ -671,7 +675,7 @@
 
 text {*
   Whenever types are given, they are stored in the @{ML SOME}s. Since types
-  are part of the inner syntax they are strings with some printing directives 
+  are part of the inner syntax they are strings with some encoded information 
   (see previous section). 
   If a syntax translation is present for a variable, then it is
   stored in the @{ML Mixfix} datastructure; no syntax translation is
@@ -701,7 +705,6 @@
   (name, map Args.dest_src attrib)
 end" "(foo_lemma, [((\"intro\", []), \<dots>), ((\"dest\", [\<dots>]), \<dots>)])"}
  
-  A name of a theorem can be quite complicated, as it can include attrinutes.
   The function @{ML opt_thm_name in SpecParse} is the ``optional'' variant of
   @{ML thm_name in SpecParse}. As can be seen each theorem name can contain some 
   attributes. If you want to print out all currently known attributes a theorem 
@@ -714,7 +717,7 @@
 \<dots>"}
 
 
-  For the inductive definitions described above only, the attibutes @{text "[intro]"} and
+  For the inductive definitions described above only the attibutes @{text "[intro]"} and
   @{text "[simp]"} make sense.
 
   \begin{readmore}