diff -r 6d2ca97a8f46 -r 7af930cd0fce src/Pure/General/file.ML
--- a/src/Pure/General/file.ML	Thu Feb 02 12:55:07 2023 +0000
+++ b/src/Pure/General/file.ML	Fri Feb 03 14:10:09 2023 +0100
@@ -89,7 +89,7 @@
 
 (* directory entries *)
 
-val exists = can OS.FileSys.modTime o platform_path;
+val exists = can OS.FileSys.fileId o platform_path;
 
 val rm = OS.FileSys.remove o platform_path;