# HG changeset patch
# User wenzelm
# Date 918059352 -3600
# Node ID 465cae203337a2e4a47e70f07bf79826d2361926
# Parent  7059f46603e26d58f9a8a449b1da2c125bb96177
tidied;

diff -r 7059f46603e2 -r 465cae203337 src/Pure/Thy/ROOT.ML
--- 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;