src/Pure/ROOT.ML
changeset 11966 8fe2ee787608
parent 11919 68b2578d4592
child 12248 f059876ef1d3
--- a/src/Pure/ROOT.ML	Sat Oct 27 23:15:52 2001 +0200
+++ b/src/Pure/ROOT.ML	Sat Oct 27 23:16:15 2001 +0200
@@ -26,7 +26,7 @@
 (*inner syntax module*)
 cd "Syntax"; use "ROOT.ML"; cd "..";
 
-(*main system*)
+(*core system*)
 use "sorts.ML";
 use "type_infer.ML";
 use "type.ML";
@@ -58,11 +58,13 @@
 (*the Isar subsystem*)
 cd "Isar"; use "ROOT.ML"; cd "..";
 
-use "goals.ML";
 use "axclass.ML";
 use "codegen.ML";
 
-(*external interfaces*)
+(*old-style goal package*)
+use "goals.ML";
+
+(*specific support for user-interfaces*)
 cd "Interface"; use "ROOT.ML"; cd "..";
 
 (*final Pure theory setup*)