--- a/CookBook/Parsing.thy	Tue Jan 27 21:22:27 2009 +0000
+++ b/CookBook/Parsing.thy	Wed Jan 28 06:29:16 2009 +0000
@@ -584,7 +584,7 @@
 
   The option @{text "-k foobar"} indicates which postfix the name of the keyword file 
   will be assigned. In the case above the file will be named @{text
-  "isar-keywords-foobar.el"}. As can be seen, this command requires log files to be
+  "isar-keywords-foobar.el"}. This command requires log files to be
   present (in order to extract the keywords from them). To generate these log
   files, we first package the code above into a separate theory file named
   @{text "Command.thy"}, say---see Figure~\ref{fig:commandtheory} for the
@@ -683,9 +683,9 @@
    $ISABELLE_LOGS/{Pure.gz,HOL.gz,Pure-ProofGeneral.gz,HOL-FoobarCommand.gz}"}
 
   The result is the file @{text "isar-keywords-foobar.el"}. It should contain
-  the string @{text "foobar"} twice (to see whether things went wrong, check
+  the string @{text "foobar"} twice.\footnote{To see whether things are fine, check
   that @{text "grep foobar"} on this file returns something
-  non-empty).  This keyword file needs to
+  non-empty.}  This keyword file needs to
   be copied into the directory @{text "~/.isabelle/etc"}. To make Isabelle
   aware of this keyword file, we have to start Isabelle with the option @{text
   "-k foobar"}, i.e.
@@ -740,7 +740,7 @@
   \isacommand{definition} and \isacommand{declare}.  In other cases,
   commands are expected to parse some arguments, for example a proposition,
   and then ``open up'' a proof in order to prove the proposition (for example
-  \isacommand{lemma}) or prove some other properties (for example in
+  \isacommand{lemma}) or prove some other properties (for example
   \isacommand{function}). To achieve this kind of behaviour, we have to use the kind
   indicator @{ML thy_goal in OuterKeyword}.
 
@@ -767,7 +767,7 @@
 end *}
 
 text {*
-  The function @{text set_up_thm} takes a string (the proposition to be
+  The function @{text set_up_thm} in Lines 2 to 7 takes a string (the proposition to be
   proved) and a context.  The context is necessary in order to be able to use
   @{ML Syntax.read_prop}, which converts a string into a proper proposition.
   In Line 6 the function @{ML Proof.theorem_i} starts the proof for the
@@ -794,6 +794,8 @@
   \isacommand{done}
   \end{isabelle}
 
+  Similarly for the other function composition combinators.
+
   
   (FIXME What does @{text "Toplevel.theory"} @{text "Toplevel.print"}?)