# HG changeset patch
# User wenzelm
# Date 1014666369 -3600
# Node ID 84eb6c75cfe352def4975811aec31e4922d13ea5
# Parent  d697091d1591ff066eb03c2b383fc28ff8bbae0f
clarify module dependencies;

diff -r d697091d1591 -r 84eb6c75cfe3 src/Pure/Isar/ROOT.ML
--- a/src/Pure/Isar/ROOT.ML	Mon Feb 25 20:33:40 2002 +0100
+++ b/src/Pure/Isar/ROOT.ML	Mon Feb 25 20:46:09 2002 +0100
@@ -37,13 +37,13 @@
 use "session.ML";
 use "isar_output.ML";
 
+(*theory syntax*)
+use "thy_header.ML";
+use "outer_syntax.ML";
+
 (*theory and proof operations*)
 use "isar_thy.ML";
 use "isar_cmd.ML";
-
-(*theory syntax*)
-use "thy_header.ML";
-use "outer_syntax.ML";
 use "isar_syn.ML";
 
 (*main ML interfaces*)
@@ -69,11 +69,11 @@
   structure OuterParse = OuterParse;
   structure Toplevel = Toplevel;
   structure Session = Session;
-  structure IsarThy = IsarThy;
   structure IsarOutput = IsarOutput;
-  structure IsarCmd = IsarCmd;
   structure ThyHeader = ThyHeader;
   structure OuterSyntax = OuterSyntax;
+  structure IsarThy = IsarThy;
+  structure IsarCmd = IsarCmd;
   structure IsarSyn = IsarSyn;
   structure Isar = Isar;
 end;