src/Pure/General/file.ML
changeset 26656 62fff5feb756
parent 26503 4dec4460244f
child 26946 0b6eff8c088d
--- a/src/Pure/General/file.ML	Tue Apr 15 16:12:13 2008 +0200
+++ b/src/Pure/General/file.ML	Tue Apr 15 16:12:15 2008 +0200
@@ -141,7 +141,7 @@
 
 fun eq paths =
   (case try (pairself (OS.FileSys.fileId o platform_path)) paths of
-    SOME ids => OS.FileSys.compare ids = EQUAL
+    SOME ids => is_equal (OS.FileSys.compare ids)
   | NONE => false);
 
 fun copy src dst =