# HG changeset patch
# User wenzelm
# Date 1257857977 -3600
# Node ID 6d5dfa64b98056c1b8aab8d49b51a72d86a50e48
# Parent  edfc35dcfe31a676f55d7b3950d860d40f34fa6e
removed obsolete name_of -- cf. decode;

diff -r edfc35dcfe31 -r 6d5dfa64b980 src/Pure/General/symbol.ML
--- 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 *)