--- a/ProgTutorial/Parsing.thy	Thu Oct 01 10:19:21 2009 +0200
+++ b/ProgTutorial/Parsing.thy	Fri Oct 02 15:38:14 2009 +0200
@@ -697,6 +697,7 @@
 | evenS: "odd n \<Longrightarrow> even (Suc n)"
 | oddS: "even n \<Longrightarrow> odd (Suc n)"
 
+
 text {*
   For this we are going to use the parser:
 *}
@@ -980,10 +981,10 @@
 
 text {* 
   but you will not see any action as we chose to implement this command to do
-  nothing. The point of this command is to only show the procedure of how
+  nothing. The point of this command is only to show the procedure of how
   to interact with ProofGeneral. A similar procedure has to be done with any 
   other new command, and also any new keyword that is introduced with 
-  @{ML_ind OuterKeyword.keyword}.
+  the function @{ML_ind keyword in OuterKeyword}. For example:
 *}
 
 ML{*val _ = OuterKeyword.keyword "blink" *}
@@ -1005,13 +1006,12 @@
 
 ML{*let
   fun trace_prop str = 
-     LocalTheory.theory (fn lthy => (tracing str; lthy))
+     LocalTheory.theory (fn ctxt => (tracing str; ctxt))
 
-  val trace_prop_parser = OuterParse.prop >> trace_prop
   val kind = OuterKeyword.thy_decl
 in
   OuterSyntax.local_theory "foobar_trace" "traces a proposition" 
-    kind trace_prop_parser
+    kind (OuterParse.prop >> trace_prop)
 end *}
 
 text {*
@@ -1036,28 +1036,28 @@
   OuterKeyword} to @{ML thy_goal in OuterKeyword} then the keyword file needs
   to be re-created!
 
-  Below we change \isacommand{foobar\_trace} so that it takes a proposition as
-  argument and then starts a proof in order to prove it. Therefore in Line 13, 
-  we set the kind indicator to @{ML thy_goal in OuterKeyword}.
+  Below we show the command \isacommand{foobar\_goal} which takes a
+  proposition as argument and then starts a proof in order to prove
+  it. Therefore in Line 9, we set the kind indicator to @{ML thy_goal in
+  OuterKeyword}.
 *}
 
 ML%linenosgray{*let
-  fun prove_prop str lthy =
+  fun goal_prop str lthy =
     let
       val prop = Syntax.read_prop lthy str
     in
       Proof.theorem_i NONE (K I) [[(prop,[])]] lthy
-    end;
+    end
   
-  val prove_prop_parser = OuterParse.prop >> prove_prop 
   val kind = OuterKeyword.thy_goal
 in
-  OuterSyntax.local_theory_to_proof "foobar_goal" "proving a proposition" 
-    kind prove_prop_parser
+  OuterSyntax.local_theory_to_proof "foobar_goal" "proves a proposition" 
+    kind (OuterParse.prop >> goal_prop)
 end *}
 
 text {*
-  The function @{text prove_prop} in Lines 2 to 7 takes a string (the proposition to be
+  The function @{text goal_prop} in Lines 2 to 7 takes a string (the proposition to be
   proved) and a context as argument.  The context is necessary in order to be able to use
   @{ML_ind  read_prop in Syntax}, which converts a string into a proper proposition.
   In Line 6 the function @{ML_ind  theorem_i in Proof} starts the proof for the
@@ -1083,6 +1083,7 @@
 done
 
 text {*
+  {\bf TBD below}
 
   (FIXME: read a name and show how to store theorems; see @{ML_ind  note in LocalTheory})