tuned signature;

--- a/src/Pure/General/symbol.scala	Fri Jun 09 14:25:00 2017 +0200
+++ b/src/Pure/General/symbol.scala	Fri Jun 09 16:59:14 2017 +0200
@@ -369,7 +369,7 @@
           ("abbrev", a) <- props.reverse
         } yield sym -> a): _*)
 
-    val codes: List[(String, Int)] =
+    val codes: List[(Symbol, Int)] =
     {
       val Code = new Properties.String("code")
       for {
@@ -500,7 +500,7 @@
   def names: Map[Symbol, String] = symbols.names
   def groups: List[(String, List[Symbol])] = symbols.groups
   def abbrevs: Multi_Map[Symbol, String] = symbols.abbrevs
-  def codes: List[(String, Int)] = symbols.codes
+  def codes: List[(Symbol, Int)] = symbols.codes
 
   def decode(text: String): String = symbols.decode(text)
   def encode(text: String): String = symbols.encode(text)