src/Pure/General/path.scala

       else if (r == 1) (List(Root("")), es)
       else if (es.isEmpty) (List(Root("")), Nil)
       else (List(root_elem(es.head)), es.tail)
     val elems = raw_elems.filterNot(s => s.isEmpty || s == ".").map(explode_elem)
 
-    new Path(norm_elems(elems.reverse ::: roots))
+    new Path(norm_elems(elems reverse_::: roots))
   }
 
   def is_wellformed(str: String): Boolean =
     try { explode(str); true } catch { case ERROR(_) => false }