--- a/src/Pure/General/file.ML Sun Jan 21 16:43:42 2007 +0100
+++ b/src/Pure/General/file.ML Sun Jan 21 16:43:44 2007 +0100
@@ -33,7 +33,6 @@
val eq: Path.T * Path.T -> bool
val copy: Path.T -> Path.T -> unit
val copy_dir: Path.T -> Path.T -> unit
- val use: Path.T -> unit
end;
structure File: FILE =
@@ -147,9 +146,4 @@
if eq (src, dst) then ()
else (system_command ("cp -r -f " ^ shell_path src ^ "/. " ^ shell_path dst); ());
-
-(* use ML files *)
-
-val use = Output.ML_errors use o platform_path;
-
end;