--- a/src/Pure/Thy/ROOT.ML Wed Feb 03 17:28:40 1999 +0100
+++ b/src/Pure/Thy/ROOT.ML Wed Feb 03 17:29:12 1999 +0100
@@ -1,20 +1,19 @@
(* Title: Pure/Thy/ROOT.ML
ID: $Id$
-This file builds the theory parser and autoloading system.
+Theory system operations.
*)
-use "use.ML";
+(*theory auto loader database*)
+use "thy_load.ML";
+use "thy_info.ML";
+use "session.ML";
+(*theory presentation*)
+use "present.ML";
+use "thm_database.ML";
+
+(*theory syntax (old format)*) (* FIXME rename to OldThy (!?) *)
use "thy_scan.ML";
use "thy_parse.ML";
use "thy_syn.ML";
-
-use "context.ML";
-
-use "thy_info.ML";
-use "browser_info.ML";
-use "thm_database.ML";
-use "thy_read.ML";
-
-open ThmDatabase ThyRead ThyInfo BrowserInfo;