diff -r 4536782969fa -r c39f83d8daeb CookBook/Parsing.thy
--- a/CookBook/Parsing.thy	Sat Feb 14 16:09:04 2009 +0000
+++ b/CookBook/Parsing.thy	Sun Feb 15 18:58:21 2009 +0000
@@ -190,7 +190,7 @@
                                "Exception ABORT raised"}
 
   then the parsing aborts and the error message @{text "foo"} is printed. In order to
-  see the error message properly, we need to prefix the parser with the function 
+  see the error message properly, you need to prefix the parser with the function 
   @{ML "Scan.error"}. For example:
 
   @{ML_response_fake [display,gray] "Scan.error (!! (fn _ => \"foo\") ($$ \"h\"))"
@@ -599,6 +599,16 @@
   (FIXME: why is intro, elim and dest treated differently from bar?) 
 *}
 
+ML{*val spec_parser = 
+    OuterParse.opt_target --
+    OuterParse.fixes -- 
+    OuterParse.for_fixes --
+    Scan.optional 
+        (OuterParse.$$$ "where" |--
+           OuterParse.!!! 
+             (OuterParse.enum1 "|" 
+                (SpecParse.opt_thm_name ":" -- OuterParse.prop))) []*}
+
 text {*
 @{ML_response [display,gray]
 "let
@@ -608,18 +618,8 @@
       \"  even0[intro]: \\\"even 0\\\" \" ^ 
       \"| evenS[intro]: \\\"odd n \<Longrightarrow> even (Suc n)\\\" \" ^ 
       \"| oddS[intro]:  \\\"even n \<Longrightarrow> odd (Suc n)\\\"\")
-
-  val parser = 
-    OuterParse.opt_target --
-    OuterParse.fixes -- 
-    OuterParse.for_fixes --
-    Scan.optional 
-        (OuterParse.$$$ \"where\" |--
-           OuterParse.!!! 
-             (OuterParse.enum1 \"|\" 
-                (SpecParse.opt_thm_name \":\" -- OuterParse.prop))) []
 in
-  parse parser input
+  parse spec_parser input
 end"
 "((((NONE, [(even, NONE, NoSyn), (odd, NONE, NoSyn)]), []),
      [((even0,\<dots>), \"\\^E\\^Ftoken\\^Eeven 0\\^E\\^F\\^E\"),