--- a/CookBook/Parsing.thy	Wed Mar 18 03:27:15 2009 +0100
+++ b/CookBook/Parsing.thy	Wed Mar 18 18:27:48 2009 +0100
@@ -618,7 +618,6 @@
 *}
 
 ML %linenosgray{*val spec_parser = 
-     OuterParse.opt_target --
      OuterParse.fixes -- 
      Scan.optional 
        (OuterParse.$$$ "where" |--
@@ -646,27 +645,17 @@
 in
   parse spec_parser input
 end"
-"(((NONE, [(even, NONE, NoSyn), (odd, NONE, NoSyn)]),
+"(([(even, NONE, NoSyn), (odd, NONE, NoSyn)],
      [((even0,\<dots>), \"\\^E\\^Ftoken\\^Eeven 0\\^E\\^F\\^E\"),
       ((evenS,\<dots>), \"\\^E\\^Ftoken\\^Eodd n \<Longrightarrow> even (Suc n)\\^E\\^F\\^E\"),
       ((oddS,\<dots>), \"\\^E\\^Ftoken\\^Eeven n \<Longrightarrow> odd (Suc n)\\^E\\^F\\^E\")]), [])"}
 
-  As you see, the result is a ``nested'' four-tuple consisting of an optional
-  locale (in this case @{ML NONE}); a list of variables with optional
-  type-annotation and syntax-annotation; and a list of rules where every rule
-  has optionally a name and an attribute.
-
+  As you see, the result is a pair consisting of a list of
+  variables with optional type-annotation and syntax-annotation, 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
-
-@{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
-  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 
+  The function @{ML OuterParse.fixes} in Line 2 of the parser reads an 
+  \isacommand{and}-separated 
   list of variables that can include optional type annotations and syntax translations. 
   For example:\footnote{Note that in the code we need to write 
   @{text "\\\"int \<Rightarrow> bool\\\""} in order to properly escape the double quotes
@@ -696,7 +685,7 @@
   The datastructre for sytax annotations is defined in @{ML_file "Pure/Syntax/mixfix.ML"}.
   \end{readmore}
 
-  Lines 4 to 8 in the function @{ML spec_parser} implement the parser for a
+  Lines 3 to 7 in the function @{ML spec_parser} implement the parser for a
   list of introduction rules, that is propositions with theorem
   annotations. The introduction rules are propositions parsed by @{ML
   OuterParse.prop}. However, they can include an optional theorem name plus
@@ -712,7 +701,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 
-  the function @{ML SpecParse.opt_thm_name} in Line 8.
+  the function @{ML SpecParse.opt_thm_name} in Line 7.
 
   \begin{readmore}
   Attributes and arguments are implemented in the files @{ML_file "Pure/Isar/attrib.ML"} 
@@ -916,7 +905,7 @@
   \isacommand{function}). To achieve this kind of behaviour, you have to use the kind
   indicator @{ML thy_goal in OuterKeyword}.  Note, however, once you change the 
   ``kind'' of a command from @{ML thy_decl in OuterKeyword} to @{ML thy_goal in OuterKeyword} 
-  then the keyword file needs to be re-created.
+  then the keyword file needs to be re-created!
 
   Below we change \isacommand{foobar} so that it takes a proposition as
   argument and then starts a proof in order to prove it. Therefore in Line 13, 
@@ -981,9 +970,9 @@
 section {* Methods *}
 
 text {*
-  Methods are one central concept in Isabelle. Methods can be applied with the command
-  \isacommand{apply}. To print out all currently known methods you can use the Isabelle
-  command. 
+  Methods are a central concept in Isabelle. They are the ones you use for example
+  in \isacommand{apply}. To print out all currently known methods you can use the 
+  Isabelle command. 
 *}
 
 print_methods
@@ -998,9 +987,10 @@
          "foobar method"
 
 text {*
-  It defines the method @{text foobar_meth} which takes no arguments and 
+  It defines the method @{text foobar_meth}, which takes no arguments (therefore the
+  parser @{ML Scan.succeed}) and 
   only applies the tactic @{thm [source] conjE} and then @{thm [source] conjI}.
-  It can be applied in the following proof
+  This method can be used in the following proof
 *}
 
 lemma shows "A \<and> B \<Longrightarrow> C \<and> D"
@@ -1013,6 +1003,9 @@
   \end{minipage} *}
 (*<*)oops(*>*)
 
+text {*
+  (FIXME: explain a version of rule-tac)
+*}
 
 (*<*)