removed obsolete name_of -- cf. decode;
--- a/src/Pure/General/symbol.ML Tue Nov 10 13:45:11 2009 +0100
+++ b/src/Pure/General/symbol.ML Tue Nov 10 13:59:37 2009 +0100
@@ -18,7 +18,6 @@
val is_symbolic: symbol -> bool
val is_printable: symbol -> bool
val is_utf8_trailer: symbol -> bool
- val name_of: symbol -> string
val eof: symbol
val is_eof: symbol -> bool
val not_eof: symbol -> bool
@@ -137,10 +136,6 @@
fun is_regular s =
not_eof s andalso s <> sync andalso s <> malformed andalso s <> end_malformed;
-fun name_of s = if is_symbolic s
- then (unsuffix ">" o unprefix "\\<") s
- else error (malformed_msg s);
-
(* ascii symbols *)