# HG changeset patch
# User wenzelm
# Date 1169394224 -3600
# Node ID fedad292f738014f2f0c8170a08bc6e10adbdd36
# Parent  c33450acd873c6cdadb8e56fb07bea330cca7359
moved File.use to ML_Context.use;

diff -r c33450acd873 -r fedad292f738 src/Pure/General/file.ML
--- 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;
diff -r c33450acd873 -r fedad292f738 src/Pure/Thy/thy_load.ML
--- a/src/Pure/Thy/thy_load.ML	Sun Jan 21 16:43:42 2007 +0100
+++ b/src/Pure/Thy/thy_load.ML	Sun Jan 21 16:43:44 2007 +0100
@@ -92,7 +92,7 @@
 fun load_file current raw_path =
   (case check_file current raw_path of
     NONE => error ("Could not find ML file " ^ quote (Path.implode raw_path))
-  | SOME (path, info) => (File.use path; (path, info)));
+  | SOME (path, info) => (ML_Context.use path; (path, info)));
 
 
 (* datatype master *)