diff -r 0364007b4bb3 -r 6e6eb8d92377 src/Pure/General/symbol.ML
--- a/src/Pure/General/symbol.ML	Wed Jun 30 09:47:16 1999 +0200
+++ b/src/Pure/General/symbol.ML	Wed Jun 30 12:22:31 1999 +0200
@@ -9,6 +9,9 @@
 sig
   type symbol
   val space: symbol
+  val sync: symbol
+  val is_sync: symbol -> bool
+  val not_sync: symbol -> bool
   val eof: symbol
   val is_eof: symbol -> bool
   val not_eof: symbol -> bool
@@ -55,11 +58,15 @@
 type symbol = string;
 
 val space = " ";
+val sync = "\\<^sync>";
 val eof = "";
 
 
 (* kinds *)
 
+fun is_sync s = s = sync;
+fun not_sync s = s <> sync;
+
 fun is_eof s = s = eof;
 fun not_eof s = s <> eof;
 val stopper = (eof, is_eof);