diff -r 0b7656c5f0e9 -r 5fb4990dfc73 src/Pure/General/path.scala
--- a/src/Pure/General/path.scala	Fri May 01 15:33:43 2015 +0200
+++ b/src/Pure/General/path.scala	Sun May 03 00:01:10 2015 +0200
@@ -18,9 +18,9 @@
   /* path elements */
 
   sealed abstract class Elem
-  private case class Root(val name: String) extends Elem
-  private case class Basic(val name: String) extends Elem
-  private case class Variable(val name: String) extends Elem
+  private case class Root(name: String) extends Elem
+  private case class Basic(name: String) extends Elem
+  private case class Variable(name: String) extends Elem
   private case object Parent extends Elem
 
   private def err_elem(msg: String, s: String): Nothing =
@@ -30,7 +30,7 @@
     if (s == "" || s == "~" || s == "~~") err_elem("Illegal", s)
     else {
       "/\\$:\"'".iterator.foreach(c =>
-        if (s.iterator.exists(_ == c))
+        if (s.iterator.contains(c))
           err_elem("Illegal character " + quote(c.toString) + " in", s))
       s
     }