--- a/src/Pure/General/symbol.ML Fri Oct 31 21:48:40 2014 +0100
+++ b/src/Pure/General/symbol.ML Fri Oct 31 22:02:49 2014 +0100
@@ -19,9 +19,6 @@
val is_eof: symbol -> bool
val not_eof: symbol -> bool
val stopper: symbol Scan.stopper
- val sync: symbol
- val is_sync: symbol -> bool
- val is_regular: symbol -> bool
val is_malformed: symbol -> bool
val malformed_msg: symbol -> string
val is_ascii: symbol -> bool
@@ -119,12 +116,6 @@
fun not_eof s = s <> eof;
val stopper = Scan.stopper (K eof) is_eof;
-(*Proof General legacy*)
-val sync = "\\<^sync>";
-fun is_sync s = s = sync;
-
-fun is_regular s = not_eof s andalso s <> sync;
-
fun is_malformed s =
String.isPrefix "\\<" s andalso not (String.isSuffix ">" s)
orelse s = "\\<>" orelse s = "\\<^>";