# HG changeset patch
# User wenzelm
# Date 1189947149 -7200
# Node ID 5c290506fbc04c9b1201842756f7a690756cd8a1
# Parent  6689effe75d1ba34d6d60329fde8d45f915329e6
tuned message;

diff -r 6689effe75d1 -r 5c290506fbc0 src/Pure/General/scan.ML
--- a/src/Pure/General/scan.ML	Sun Sep 16 14:52:28 2007 +0200
+++ b/src/Pure/General/scan.ML	Sun Sep 16 14:52:29 2007 +0200
@@ -221,7 +221,7 @@
 
 fun finite' (stopper, is_stopper) scan (state, input) =
   let
-    fun lost () = raise ABORT "Scanner bug: lost stopper of finite scan!";
+    fun lost () = raise ABORT "Bad scanner: lost stopper of finite scan!";
 
     fun stop [] = lost ()
       | stop lst =