# HG changeset patch
# User wenzelm
# Date 1218109492 -7200
# Node ID 1ae745357856160206e34590d967bd735fc42a9a
# Parent  5df443dd9deb50f2088d71da305ba9f0e08d7113
export not_eof;

diff -r 5df443dd9deb -r 1ae745357856 src/Pure/General/symbol.ML
--- a/src/Pure/General/symbol.ML	Thu Aug 07 13:44:47 2008 +0200
+++ b/src/Pure/General/symbol.ML	Thu Aug 07 13:44:52 2008 +0200
@@ -21,6 +21,7 @@
   val is_utf8_trailer: symbol -> bool
   val eof: symbol
   val is_eof: symbol -> bool
+  val not_eof: symbol -> bool
   val stopper: symbol Scan.stopper
   val sync: symbol
   val is_sync: symbol -> bool