# HG changeset patch
# User wenzelm
# Date 1244626849 -7200
# Node ID 2db8db85c053bf2f1cb6fd7ea470d5d2049ce528
# Parent  398c0f48a99e73045d8ed3418861a88db963bbb6
tuned;

diff -r 398c0f48a99e -r 2db8db85c053 src/Pure/General/symbol.scala
--- a/src/Pure/General/symbol.scala	Wed Jun 10 11:31:36 2009 +0200
+++ b/src/Pure/General/symbol.scala	Wed Jun 10 11:40:49 2009 +0200
@@ -134,7 +134,7 @@
           val ch = new String(Character.toChars(code))
         } yield (sym, ch)
       (new Recoder(mapping),
-       new Recoder(for ((x, y) <- mapping) yield (y, x)))
+       new Recoder(mapping map { case (x, y) => (y, x) }))
     }
 
     def decode(text: String) = decoder.recode(text)