clarified according to ML version;

--- a/src/Pure/General/path.scala	Sat Apr 12 21:59:30 2014 +0200
+++ b/src/Pure/General/path.scala	Sun Apr 13 15:32:03 2014 +0200
@@ -165,7 +165,7 @@
     val (prefix, base) = split_path
     base match {
       case Ext(b, e) => (prefix + Path.basic(b), e)
-      case _ => (Path.basic(base), "")
+      case _ => (prefix + Path.basic(base), "")
     }
   }