src/Pure/General/path.ML
changeset 33037 b22e44496dc2
parent 29606 fedb8be05f24
child 33038 8f9594c31de4
     1.1 --- a/src/Pure/General/path.ML	Tue Oct 20 13:37:56 2009 +0200
     1.2 +++ b/src/Pure/General/path.ML	Tue Oct 20 16:13:01 2009 +0200
     1.3 @@ -42,7 +42,7 @@
     1.4    | check_elem (chs as ["~"]) = err_elem "Illegal" chs
     1.5    | check_elem (chs as ["~", "~"]) = err_elem "Illegal" chs
     1.6    | check_elem chs =
     1.7 -      (case ["/", "\\", "$", ":"] inter_string chs of
     1.8 +      (case gen_inter (op =) (["/", "\\", "$", ":"], chs) of
     1.9          [] => chs
    1.10        | bads => err_elem ("Illegal character(s) " ^ commas_quote bads ^ " in") chs);
    1.11