# HG changeset patch
# User wenzelm
# Date 1497020354 -7200
# Node ID 70d3d0818d42bf053aeefb1b552e7c11f79f2445
# Parent  d244a895da50fd5d0fec898df7b7428c9381d7e8
tuned signature;

diff -r d244a895da50 -r 70d3d0818d42 src/Pure/General/symbol.scala
--- 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)