--- a/src/Pure/library.ML Wed Aug 06 00:29:02 1997 +0200
+++ b/src/Pure/library.ML Wed Aug 06 00:29:54 1997 +0200
@@ -873,6 +873,8 @@
(rm_points (space_explode "/" (tack_on cwd file)) [])
end;
+fun file_exists file = (file_info file <> "");
+
(** misc functions **)