src/Pure/General/symbol.scala

--- a/src/Pure/General/symbol.scala	Tue Aug 26 16:36:11 2008 +0200
+++ b/src/Pure/General/symbol.scala	Tue Aug 26 16:36:30 2008 +0200
@@ -148,7 +148,7 @@
 
     private def init_recoders() = {
       val list = symbols.elements.toList.map(get_code)
-      decoder = new Recoder(list ::: (for ((x, y) <- list) yield ("\\" + x, y)))
+      decoder = new Recoder(list ++ (for ((x, y) <- list) yield ("\\" + x, y)))
       encoder = new Recoder(for ((x, y) <- list) yield (y, x))
     }