# HG changeset patch
# User wenzelm
# Date 879348167 -3600
# Node ID 523f6bea9fd742f42bdb0a1d3c8dd992a6355685
# Parent  cef5ef41e70d9d417ce077ccdc5837cf75e4349a
added file.ML, use.ML;
removed symbol_input.ML;

diff -r cef5ef41e70d -r 523f6bea9fd7 src/Pure/Thy/ROOT.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;