# HG changeset patch
# User wenzelm
# Date 1546182369 -3600
# Node ID 612a02019f489938b1c0db7abc4301933fef4ddf
# Parent  415dc92050a624ae94afe47e2a46848ab46fa738
tuned;

diff -r 415dc92050a6 -r 612a02019f48 src/Pure/General/path.ML
--- a/src/Pure/General/path.ML	Sun Dec 30 15:36:43 2018 +0100
+++ b/src/Pure/General/path.ML	Sun Dec 30 16:06:09 2018 +0100
@@ -59,8 +59,8 @@
 val check_elem = tap (fn s =>
   if member (op =) illegal_elem s then err_elem "Illegal" s
   else
-    illegal_char |> List.app (fn c =>
-      if exists_string (fn c' => c = c') s then
+    (s, ()) |-> fold_string (fn c => fn () =>
+      if member (op =) illegal_char c then
         err_elem ("Illegal character " ^ quote c ^ " in") s
       else ()));
 
diff -r 415dc92050a6 -r 612a02019f48 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