moved theory presentation to Isar/ROOT.ML;

--- a/src/Pure/Isar/ROOT.ML	Sun Apr 09 18:51:15 2006 +0200
+++ b/src/Pure/Isar/ROOT.ML	Sun Apr 09 18:51:16 2006 +0200
@@ -5,13 +5,22 @@
 Isar -- Intelligible Semi-Automated Reasoning for Isabelle.
 *)
 
-(*basic proof engine*)
+(*proof context*)
 use "object_logic.ML";
 use "rule_cases.ML";
 use "auto_bind.ML";
 use "local_syntax.ML";
 use "proof_context.ML";
 use "local_defs.ML";
+
+(*theory presentation*)
+use "../Thy/html.ML";
+use "../Thy/latex.ML";
+use "../Thy/present.ML";
+use "../Thy/thm_deps.ML";
+use "../Thy/thm_database.ML";
+
+(*basic proof engine*)
 use "proof_display.ML";
 use "args.ML";
 use "attrib.ML";

--- a/src/Pure/ROOT.ML	Sun Apr 09 18:51:15 2006 +0200
+++ b/src/Pure/ROOT.ML	Sun Apr 09 18:51:16 2006 +0200
@@ -66,15 +66,6 @@
 (*theory syntax*)
 use "Isar/outer_lex.ML";
 
-(*theory presentation*)
-use "Thy/html.ML";
-use "Thy/latex.ML";
-use "Thy/present.ML";
-use "Thy/thm_deps.ML";
-
-(*theorem database ML interface*)
-use "Thy/thm_database.ML";
-
 (*the Isar system*)
 cd "Isar"; use "ROOT.ML"; cd "..";