load locale.ML late (after proof.ML);
tuned module arrangement;

--- a/src/Pure/Isar/ROOT.ML	Tue Sep 13 22:19:31 2005 +0200
+++ b/src/Pure/Isar/ROOT.ML	Tue Sep 13 22:19:32 2005 +0200
@@ -7,23 +7,24 @@
 
 (*basic proof engine*)
 use "object_logic.ML";
+use "rule_cases.ML";
 use "auto_bind.ML";
-use "rule_cases.ML";
 use "proof_context.ML";
+use "proof_display.ML";
 use "context_rules.ML";
 use "args.ML";
 use "attrib.ML";
-use "locale.ML";
+use "skip_proof.ML";
 use "method.ML";
 use "proof.ML";
-use "proof_history.ML";
 use "net_rules.ML";
 use "induct_attrib.ML";
 
-(*derived proof elements*)
+(*derived theory and proof elements*)
+use "constdefs.ML";
+use "locale.ML";
+use "obtain.ML";
 use "calculation.ML";
-use "obtain.ML";
-use "skip_proof.ML";
 
 (*outer syntax*)
 use "antiquote.ML";
@@ -31,6 +32,7 @@
 use "outer_keyword.ML";
 
 (*toplevel environment*)
+use "proof_history.ML";
 use "toplevel.ML";
 
 (*theory presentation*)
@@ -43,9 +45,8 @@
 use "outer_syntax.ML";
 
 (*theory and proof operations*)
-use "isar_thy.ML";
-use "constdefs.ML";
 use "../simplifier.ML";
 use "find_theorems.ML";
+use "isar_thy.ML";
 use "isar_cmd.ML";
 use "isar_syn.ML";