src/Pure/ROOT.ML
changeset 24235 aea5c389a2f5
parent 24113 ec9e75a46e16
child 24257 15a43b494878
--- a/src/Pure/ROOT.ML	Sun Aug 12 19:00:58 2007 +0200
+++ b/src/Pure/ROOT.ML	Mon Aug 13 00:17:54 2007 +0200
@@ -23,6 +23,8 @@
 use "term.ML";
 use "term_subst.ML";
 use "General/pretty.ML";
+use "Syntax/lexicon.ML";
+use "Syntax/simple_syntax.ML";
 use "sorts.ML";
 use "type.ML";
 use "context.ML";
@@ -32,7 +34,6 @@
 use "type_infer.ML";
 
 (*inner syntax module*)
-use "Syntax/lexicon.ML";
 use "Syntax/ast.ML";
 use "Syntax/syn_ext.ML";
 use "Syntax/parser.ML";