diff -r e5990cd1b51a -r ee139d9d7ab8 ProgTutorial/Parsing.thy
--- a/ProgTutorial/Parsing.thy	Wed Jul 22 09:53:35 2009 +0200
+++ b/ProgTutorial/Parsing.thy	Wed Jul 22 13:59:37 2009 +0200
@@ -798,7 +798,9 @@
                   OuterParse.!!! (OuterParse.$$$ "|"))))) [] *}
 text_raw {*
   \end{isabelle}
-  Both parsers accept the same input, but if you look closely, you can notice 
+  Both parsers accept the same input% that's not true:
+  % spec_parser accepts input that is refuted by spec_parser'
+  , but if you look closely, you can notice 
   an additional  ``tail'' (Lines 8 to 10) in @{ML spec_parser'}. What is the purpose of 
   this additional ``tail''?
   \end{exercise}