diff -r 8db9195bb3e9 -r 2d9198bcb850 CookBook/Parsing.thy
--- a/CookBook/Parsing.thy	Mon Feb 23 00:27:27 2009 +0000
+++ b/CookBook/Parsing.thy	Mon Feb 23 17:08:15 2009 +0000
@@ -429,7 +429,7 @@
 in 
   (Scan.dest_lexicon commands, Scan.dest_lexicon keywords)
 end" 
-"([\"}\", \"{\", \<dots>],[\"\<rightleftharpoons>\", \"\<leftharpoondown>\", \<dots>])"}
+"([\"}\", \"{\", \<dots>], [\"\<rightleftharpoons>\", \"\<leftharpoondown>\", \<dots>])"}
 
   The parser @{ML "OuterParse.$$$"} parses a single keyword. For example: