diff -r 15f001295a7b -r 5c16895d548b src/Pure/General/path.ML
--- a/src/Pure/General/path.ML	Tue Mar 21 12:18:13 2006 +0100
+++ b/src/Pure/General/path.ML	Tue Mar 21 12:18:15 2006 +0100
@@ -118,7 +118,7 @@
         "$" :: cs => variable_elem cs
       | cs => basic_elem cs);
 
-val unpack_elems = map unpack_elem o filter_out (equal "" orf equal ".");
+val unpack_elems = map unpack_elem o filter_out (fn c => c = "" orelse c = ".");
 
 fun unpack str = Path (norm
   (case space_explode "/" str of
@@ -140,7 +140,7 @@
   | ext e path = split_path (fn (prfx, s) => append (Path prfx) (basic (s ^ "." ^ e))) path;
 
 val split_ext = split_path (fn (prfx, s) => apfst (append (Path prfx))
-  (case take_suffix (not_equal ".") (explode s) of
+  (case take_suffix (fn c => c <> ".") (explode s) of
     ([], _) => (Path [Basic s], "")
   | (cs, e) => (Path [Basic (implode (Library.take (length cs - 1, cs)))], implode e)));