type.ML now before Syntax module;
authorwenzelm
Fri, 21 May 2004 21:21:38 +0200
changeset 14781 2be804d1dda9
parent 14780 949a3f558a43
child 14782 d6ce35a1c386
type.ML now before Syntax module;
src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Fri May 21 21:21:12 2004 +0200
+++ b/src/Pure/ROOT.ML	Fri May 21 21:21:38 2004 +0200
@@ -21,15 +21,17 @@
 (*basic tools*)
 use "library.ML";
 cd "General"; use "ROOT.ML"; cd "..";
+
+(*fundamental structures*)
 use "term.ML";
+use "sorts.ML";
+use "type.ML";
 
 (*inner syntax module*)
 cd "Syntax"; use "ROOT.ML"; cd "..";
 
 (*core system*)
-use "sorts.ML";
 use "type_infer.ML";
-use "type.ML";
 use "sign.ML";
 use "envir.ML";
 use "pattern.ML";