--- a/CookBook/Parsing.thy	Fri Mar 13 16:57:16 2009 +0100
+++ b/CookBook/Parsing.thy	Sat Mar 14 00:48:22 2009 +0100
@@ -613,14 +613,6 @@
 | evenS: "odd n \<Longrightarrow> even (Suc n)"
 | oddS: "even n \<Longrightarrow> odd (Suc n)"
 
-text {* and *}
-
-simple_inductive 
-  trcl\<iota> for R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
-where
-  base: "trcl\<iota> R x x"
-| step: "trcl\<iota> R x y \<Longrightarrow> R y z \<Longrightarrow> trcl\<iota> R x z"
-
 text {*
   For this we are going to use the parser:
 *}
@@ -628,7 +620,6 @@
 ML %linenosgray{*val spec_parser = 
      OuterParse.opt_target --
      OuterParse.fixes -- 
-     OuterParse.for_fixes --
      Scan.optional 
        (OuterParse.$$$ "where" |--
           OuterParse.!!! 
@@ -655,16 +646,16 @@
 in
   parse spec_parser input
 end"
-"((((NONE, [(even, NONE, NoSyn), (odd, NONE, NoSyn)]), []),
+"(((NONE, [(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; 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.
+  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.
+
 
   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
@@ -705,15 +696,7 @@
   The datastructre for sytax annotations is defined in @{ML_file "Pure/Syntax/mixfix.ML"}.
   \end{readmore}
 
-  Similarly, the function @{ML OuterParse.for_fixes} in Line 4: it reads the
-  same \isacommand{and}-separated list of variables as @{ML "fixes" in OuterParse}, 
-  but requires that this list is prefixed by the keyword \isacommand{for}.
-
-@{ML_response [display,gray]
-"parse OuterParse.for_fixes (filtered_input \"for foo and bar and blink\")"
-"([(foo, NONE, NoSyn), (bar, NONE, NoSyn), (blink, NONE, NoSyn)],[])"}  
-
-  Lines 5 to 9 in the function @{ML spec_parser} implement the parser for a
+  Lines 4 to 8 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
@@ -729,7 +712,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 9.
+  the function @{ML SpecParse.opt_thm_name} in Line 8.
 
   \begin{readmore}
   Attributes and arguments are implemented in the files @{ML_file "Pure/Isar/attrib.ML"}