# HG changeset patch
# User berghofe
# Date 870820194 -7200
# Node ID 5d7073700fbc2d4473adfd991d3ca266336d4d7c
# Parent  d372fb6ec393e93b58ed7985e208aa1708c13fa7
Added function "file_exists".

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 **)