| changeset 59058 | a78612c67ec0 |
| parent 56533 | cd8b6d849b6a |
| child 60970 | e08d868ceca9 |
--- 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);