src/Pure/General/path.ML

--- a/src/Pure/General/path.ML	Tue Oct 20 13:37:56 2009 +0200
+++ b/src/Pure/General/path.ML	Tue Oct 20 16:13:01 2009 +0200
@@ -42,7 +42,7 @@
   | check_elem (chs as ["~"]) = err_elem "Illegal" chs
   | check_elem (chs as ["~", "~"]) = err_elem "Illegal" chs
   | check_elem chs =
-      (case ["/", "\\", "$", ":"] inter_string chs of
+      (case gen_inter (op =) (["/", "\\", "$", ":"], chs) of
         [] => chs
       | bads => err_elem ("Illegal character(s) " ^ commas_quote bads ^ " in") chs);