src/Pure/ROOT.ML

--- a/src/Pure/ROOT.ML	Mon Oct 22 17:58:37 2001 +0200
+++ b/src/Pure/ROOT.ML	Mon Oct 22 17:58:56 2001 +0200
@@ -45,20 +45,12 @@
 use "pure_thy.ML";
 use "drule.ML";
 use "meta_simplifier.ML";
-use "locale.ML";
 use "tctical.ML";
 use "search.ML";
 use "tactic.ML";
-use "goals.ML";
-use "object_logic.ML";
 
 (*proof term operations*)
-cd "Proof";
-use "reconstruct.ML";
-use "proof_syntax.ML";
-use "proof_rewrite_rules.ML";
-use "proofchecker.ML";
-cd "..";
+cd "Proof"; use "ROOT.ML"; cd "..";
 
 (*theory system operations*)
 cd "Thy"; use "ROOT.ML"; cd "..";
@@ -66,9 +58,8 @@
 (*the Isar subsystem*)
 cd "Isar"; use "ROOT.ML"; cd "..";
 
+use "goals.ML";
 use "axclass.ML";
-
-(*code generator*)
 use "codegen.ML";
 
 (*external interfaces*)