now uses SymbolInput.use;

--- a/src/Pure/Thy/thy_read.ML	Mon Dec 16 10:02:48 1996 +0100
+++ b/src/Pure/Thy/thy_read.ML	Mon Dec 16 10:03:30 1996 +0100
@@ -747,7 +747,7 @@
           init_thyinfo ();
           delete_thms tname;
           read_thy tname thy_file;
-          use (out_name tname);
+          SymbolInput.use (out_name tname);
           save_data true;
 
           (*Store axioms of theory
@@ -773,7 +773,7 @@
 
        if ml_file = "" then ()
        else (writeln ("Reading \"" ^ name ^ ".ML\"");
-             use ml_file);
+             SymbolInput.use ml_file);
        save_data false;
 
        (*Store theory again because it could have been redefined*)