diff -r 5b649fb2f2e1 -r a78612c67ec0 src/Pure/General/file.ML
--- a/src/Pure/General/file.ML	Wed Nov 26 16:55:43 2014 +0100
+++ b/src/Pure/General/file.ML	Wed Nov 26 20:05:34 2014 +0100
@@ -167,7 +167,7 @@
 (* eq *)
 
 fun eq paths =
-  (case try (pairself (OS.FileSys.fileId o platform_path)) paths of
+  (case try (apply2 (OS.FileSys.fileId o platform_path)) paths of
     SOME ids => is_equal (OS.FileSys.compare ids)
   | NONE => false);