diff -r d372fb6ec393 -r 5d7073700fbc src/Pure/library.ML
--- 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 **)