# HG changeset patch
# User wenzelm
# Date 1218136381 -7200
# Node ID d639ec73d360e385649396e3124cb79c6da87e58
# Parent  cd5ae3dbd30e66b24c0bd1d6da14575648b5c901
tuned;

diff -r cd5ae3dbd30e -r d639ec73d360 src/Pure/General/scan.ML
--- a/src/Pure/General/scan.ML	Thu Aug 07 21:07:57 2008 +0200
+++ b/src/Pure/General/scan.ML	Thu Aug 07 21:13:01 2008 +0200
@@ -292,7 +292,7 @@
             SOME (tip, lex) =>
               let val path' = c :: path
               in scan path' (if tip then SOME (path', cs) else res) lex cs end
-          | NONE => finish res)
+          | NONE => finish res);
   in scan [] NONE lexicon end;