added assert;
tuned;

--- a/src/Pure/General/file.ML	Tue Oct 11 13:30:17 2005 +0200
+++ b/src/Pure/General/file.ML	Tue Oct 11 14:02:32 2005 +0200
@@ -19,6 +19,12 @@
   val tmp_path: Path.T -> Path.T
   val isatool: string -> int
   val system_command: string -> unit
+  eqtype info
+  val info: Path.T -> info option
+  val exists: Path.T -> bool
+  val assert: Path.T -> unit
+  val rm: Path.T -> unit
+  val mkdir: Path.T -> unit
   val read: Path.T -> string
   val write: Path.T -> string -> unit
   val append: Path.T -> string -> unit
@@ -27,11 +33,6 @@
   val eq: Path.T * Path.T -> bool
   val copy: Path.T -> Path.T -> unit
   val copy_dir: Path.T -> Path.T -> unit
-  eqtype info
-  val info: Path.T -> info option
-  val exists: Path.T -> bool
-  val rm: Path.T -> unit
-  val mkdir: Path.T -> unit
   val use: Path.T -> unit
 end;
 
@@ -93,6 +94,10 @@
 
 val exists = is_some o info;
 
+fun assert path =
+  if exists path then ()
+  else error ("No such file or directory: " ^ quote (Path.pack path));
+
 val rm = OS.FileSys.remove o platform_path;
 
 fun mkdir path = system_command ("mkdir -p " ^ shell_path path);