removed obsolete name_of -- cf. decode;
authorwenzelm
Tue, 10 Nov 2009 13:59:37 +0100
changeset 33548 6d5dfa64b980
parent 33547 edfc35dcfe31
child 33549 39f2855ce41b
removed obsolete name_of -- cf. decode;
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 *)