# HG changeset patch
# User wenzelm
# Date 850727010 -3600
# Node ID 7becd4dd5ca7143245dbf0b3f029c0d9ac1b7461
# Parent  e1b946f9c8bec2817331b9546d9d2cc0900f2f86
now uses SymbolInput.use;

diff -r e1b946f9c8be -r 7becd4dd5ca7 src/Pure/Thy/thy_read.ML
--- 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*)