--- a/src/Pure/General/symbol.ML Mon Aug 04 21:24:15 2008 +0200
+++ b/src/Pure/General/symbol.ML Mon Aug 04 21:24:17 2008 +0200
@@ -21,7 +21,7 @@
val is_utf8_trailer: symbol -> bool
val eof: symbol
val is_eof: symbol -> bool
- val stopper: symbol * (symbol -> bool)
+ val stopper: symbol Scan.stopper
val sync: symbol
val is_sync: symbol -> bool
val malformed: symbol
@@ -120,7 +120,7 @@
val eof = "";
fun is_eof s = s = eof;
fun not_eof s = s <> eof;
-val stopper = (eof, is_eof);
+val stopper = Scan.stopper (K eof) is_eof;
val sync = "\\<^sync>";
fun is_sync s = s = sync;