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

     2.1 --- a/src/Pure/General/xml.scala	Tue Aug 26 16:36:11 2008 +0200
     2.2 +++ b/src/Pure/General/xml.scala	Tue Aug 26 16:36:30 2008 +0200
     2.3 @@ -33,7 +33,7 @@
     2.4      case Nil => None
     2.5      case t :: ts => get_next(t) match {
     2.6        case None => get_nexts(ts)
     2.7 -      case Some((s, r)) => Some((s, r ::: ts))
     2.8 +      case Some((s, r)) => Some((s, r ++ ts))
     2.9      }
    2.10    }
    2.11