src/Pure/General/path.ML

 
 fun check_elem (chs as []) = err_elem "Illegal" chs
   | check_elem (chs as ["~"]) = err_elem "Illegal" chs
   | check_elem (chs as ["~", "~"]) = err_elem "Illegal" chs
   | check_elem chs =
-      (case inter (op =) (["/", "\\", "$", ":"], chs) of
+      (case inter (op =) ["/", "\\", "$", ":"] chs of
         [] => chs
       | bads => err_elem ("Illegal character(s) " ^ commas_quote bads ^ " in") chs);
 
 val basic_elem = Basic o implode o check_elem;
 val variable_elem = Variable o implode o check_elem;