# HG changeset patch
# User wenzelm
# Date 1169240902 -3600
# Node ID 4a65d2f4d0b59ffb93e4025b9ebd59230cf37ce2
# Parent  6a90ac654c6d641d19777eb70dd0393e4a98be0d
renamed Isar/isar_output.ML to Thy/thy_output.ML;
renamed Isar/term_style.ML to Thy/term_style.ML;
renamed Isar/thy_header.ML to Thy/thy_header.ML;
added Isar/spec_parse.ML;
added Thy/ml_context.ML;
load outer_parse.ML early, moved later parts to spec_parse.ML;
tuned order;

diff -r 6a90ac654c6d -r 4a65d2f4d0b5 src/Pure/Isar/ROOT.ML
--- a/src/Pure/Isar/ROOT.ML	Fri Jan 19 22:08:21 2007 +0100
+++ b/src/Pure/Isar/ROOT.ML	Fri Jan 19 22:08:22 2007 +0100
@@ -13,7 +13,17 @@
 use "proof_context.ML";
 use "local_defs.ML";
 
-(*theory presentation*)
+(*outer syntax*)
+use "outer_lex.ML";
+use "args.ML";
+use "outer_parse.ML";
+use "outer_keyword.ML";
+use "antiquote.ML";
+
+(*theory sources*)
+use "../Thy/ml_context.ML";
+use "../Thy/thy_load.ML";
+use "../Thy/thy_info.ML";
 use "../Thy/html.ML";
 use "../Thy/latex.ML";
 use "../Thy/present.ML";
@@ -22,7 +32,6 @@
 
 (*basic proof engine*)
 use "proof_display.ML";
-use "args.ML";
 use "attrib.ML";
 use "context_rules.ML";
 use "skip_proof.ML";
@@ -37,26 +46,22 @@
 use "calculation.ML";
 use "obtain.ML";
 use "locale.ML";
+use "spec_parse.ML";
 use "../axclass.ML";
 use "theory_target.ML";
 use "specification.ML";
 use "constdefs.ML";
 
-(*outer syntax*)
-use "antiquote.ML";
-use "outer_parse.ML";
-use "outer_keyword.ML";
-
 (*toplevel environment*)
 use "proof_history.ML";
 use "toplevel.ML";
 
 (*theory presentation*)
-use "term_style.ML";
-use "isar_output.ML";
+use "../Thy/term_style.ML";
+use "../Thy/thy_output.ML";
 
 (*theory syntax*)
-use "thy_header.ML";
+use "../Thy/thy_header.ML";
 use "session.ML";
 use "../old_goals.ML";
 use "outer_syntax.ML";