--- 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;