diff -r ce0f60d0351e -r 03145998190b ProgTutorial/Parsing.thy
--- a/ProgTutorial/Parsing.thy	Sat May 30 23:58:05 2009 +0200
+++ b/ProgTutorial/Parsing.thy	Sun May 31 00:39:17 2009 +0200
@@ -288,7 +288,6 @@
   where the function @{ML [index] not_eof in Symbol} ensures that we do not read beyond the 
   end of the input string (i.e.~stopper symbol).
 
-  \indexdef{unless@ {\tt\slshape{unless}}}{in {\tt\slshape Scan}}
   The function @{ML "Scan.unless p q" for p q} takes two parsers: if the first one can 
   parse the input, then the whole parser fails; if not, then the second is tried. Therefore