added file.ML, use.ML;
removed symbol_input.ML;

--- a/src/Pure/Thy/ROOT.ML	Wed Nov 12 16:22:10 1997 +0100
+++ b/src/Pure/Thy/ROOT.ML	Wed Nov 12 16:22:47 1997 +0100
@@ -7,6 +7,8 @@
 *)
 
 use "path.ML";
+use "file.ML";
+use "use.ML";
 
 use "thy_scan.ML";
 use "thy_parse.ML";
@@ -15,11 +17,9 @@
 use "thy_info.ML";
 use "browser_info.ML";
 use "thm_database.ML";
-
-use "symbol_input.ML";
 use "thy_read.ML";
 
-open ThmDatabase ThyRead ThyInfo BrowserInfo SymbolInput;
+open ThmDatabase ThyRead ThyInfo BrowserInfo;