src/Pure/ROOT.ML
changeset 39508 dfacdb01e1ec
parent 39290 44e4d8dfd6bf
child 39557 fe5722fce758
--- a/src/Pure/ROOT.ML	Fri Sep 17 20:18:27 2010 +0200
+++ b/src/Pure/ROOT.ML	Fri Sep 17 20:42:26 2010 +0200
@@ -96,13 +96,13 @@
 use "old_term.ML";
 use "General/pretty.ML";
 use "context.ML";
+use "config.ML";
 use "context_position.ML";
 use "sorts.ML";
 use "type.ML";
 use "logic.ML";
 use "Syntax/lexicon.ML";
 use "Syntax/simple_syntax.ML";
-use "config.ML";
 
 
 (* inner syntax *)