# HG changeset patch
# User wenzelm
# Date 1005261429 -3600
# Node ID a08c61932501e97a51cfd433e8844940980350ac
# Parent  fab22bdb1496d9ee338a634bfa7639bb1766c724
File.use;

diff -r fab22bdb1496 -r a08c61932501 src/Pure/Isar/session.ML
--- a/src/Pure/Isar/session.ML	Fri Nov 09 00:16:52 2001 +0100
+++ b/src/Pure/Isar/session.ML	Fri Nov 09 00:17:09 2001 +0100
@@ -84,7 +84,7 @@
       (init reset parent name;
        Present.init build info doc doc_graph (path ()) name
          (if dump = "" then None else Some (Path.unpack dump)) (get_rpath rpath_str) verbose;
-       File.symbol_use root_file;
+       File.use root_file;
        finish ()))) ()
   handle exn => (writeln (Toplevel.exn_message exn); exit 1);
 
diff -r fab22bdb1496 -r a08c61932501 src/Pure/Thy/thy_load.ML
--- a/src/Pure/Thy/thy_load.ML	Fri Nov 09 00:16:52 2001 +0100
+++ b/src/Pure/Thy/thy_load.ML	Fri Nov 09 00:17:09 2001 +0100
@@ -88,7 +88,7 @@
 fun load_file raw_path =
   (case check_file raw_path of
     None => error ("Could not find ML file " ^ quote (Path.pack raw_path))
-  | Some (path, info) => (File.symbol_use path; (path, info)));
+  | Some (path, info) => (File.use path; (path, info)));
 
 
 (* datatype master *)
diff -r fab22bdb1496 -r a08c61932501 src/Pure/Thy/thy_syn.ML
--- a/src/Pure/Thy/thy_syn.ML	Fri Nov 09 00:16:52 2001 +0100
+++ b/src/Pure/Thy/thy_syn.ML	Fri Nov 09 00:17:09 2001 +0100
@@ -56,7 +56,7 @@
     val txt_out = ThyParse.parse_thy (! syntax) chs;
   in
     File.write tmp_path txt_out;
-    File.symbol_use tmp_path;
+    File.use tmp_path;
     if ! delete_tmpfiles then File.rm tmp_path else ()
   end;