src/Pure/General/path.scala

--- a/src/Pure/General/path.scala	Sun Dec 30 15:36:43 2018 +0100
+++ b/src/Pure/General/path.scala	Sun Dec 30 16:06:09 2018 +0100
@@ -32,7 +32,7 @@
   private def check_elem(s: String): String =
     if (illegal_elem.contains(s)) err_elem("Illegal", s)
     else {
-      for (c <- illegal_char if s.contains(c)) {
+      for (c <- s if illegal_char.contains(c)) {
         err_elem("Illegal character " + quote(c.toString) + " in", s)
       }
       s