src/Pure/General/path.ML
changeset 19305 5c16895d548b
parent 17827 b32fad049413
child 19482 9f11af8f7ef9
     1.1 --- a/src/Pure/General/path.ML	Tue Mar 21 12:18:13 2006 +0100
     1.2 +++ b/src/Pure/General/path.ML	Tue Mar 21 12:18:15 2006 +0100
     1.3 @@ -118,7 +118,7 @@
     1.4          "$" :: cs => variable_elem cs
     1.5        | cs => basic_elem cs);
     1.6  
     1.7 -val unpack_elems = map unpack_elem o filter_out (equal "" orf equal ".");
     1.8 +val unpack_elems = map unpack_elem o filter_out (fn c => c = "" orelse c = ".");
     1.9  
    1.10  fun unpack str = Path (norm
    1.11    (case space_explode "/" str of
    1.12 @@ -140,7 +140,7 @@
    1.13    | ext e path = split_path (fn (prfx, s) => append (Path prfx) (basic (s ^ "." ^ e))) path;
    1.14  
    1.15  val split_ext = split_path (fn (prfx, s) => apfst (append (Path prfx))
    1.16 -  (case take_suffix (not_equal ".") (explode s) of
    1.17 +  (case take_suffix (fn c => c <> ".") (explode s) of
    1.18      ([], _) => (Path [Basic s], "")
    1.19    | (cs, e) => (Path [Basic (implode (Library.take (length cs - 1, cs)))], implode e)));
    1.20