# HG changeset patch
# User wenzelm
# Date 1261074612 -3600
# Node ID 2b9cdf23c1882666267b2868ae2acfc38727689c
# Parent  9274a44358c4341ced87ea9a884e9be0ab21dd48
tuned signature;

diff -r 9274a44358c4 -r 2b9cdf23c188 src/Pure/General/symbol.scala
--- a/src/Pure/General/symbol.scala	Thu Dec 17 15:38:58 2009 +0100
+++ b/src/Pure/General/symbol.scala	Thu Dec 17 19:30:12 2009 +0100
@@ -214,7 +214,7 @@
        new Recoder(mapping map { case (x, y) => (y, x) }))
     }
 
-    def decode(text: String) = decoder.recode(text)
-    def encode(text: String) = encoder.recode(text)
+    def decode(text: String): String = decoder.recode(text)
+    def encode(text: String): String = encoder.recode(text)
   }
 }