src/Pure/General/path.scala

       case (Parent, Basic(_) :: rest) => rest
       case _ => y :: xs
     }
 
   private def norm_elems(elems: List[Elem]): List[Elem] =
-    (elems :\ (Nil: List[Elem]))(apply_elem)
+    elems.foldRight(Nil: List[Elem])(apply_elem)
 
   private def implode_elem(elem: Elem, short: Boolean): String =
     elem match {
       case Root("") => ""
       case Root(s) => "//" + s

   def is_absolute: Boolean = elems.nonEmpty && elems.last.isInstanceOf[Path.Root]
   def is_root: Boolean = elems match { case List(Path.Root(_)) => true case _ => false }
   def is_basic: Boolean = elems match { case List(Path.Basic(_)) => true case _ => false }
   def starts_basic: Boolean = elems.nonEmpty && elems.last.isInstanceOf[Path.Basic]
 
-  def +(other: Path): Path = new Path((other.elems :\ elems)(Path.apply_elem))
+  def +(other: Path): Path = new Path(other.elems.foldRight(elems)(Path.apply_elem))
 
 
   /* implode */
 
   private def gen_implode(short: Boolean): String =