diff -r da9ae7774513 -r b906dd1de855 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Mon Sep 29 12:32:00 2008 +0200
+++ b/src/Pure/ROOT.ML	Mon Sep 29 14:41:22 2008 +0200
@@ -29,9 +29,10 @@
 use "term_subst.ML";
 use "logic.ML";
 use "General/pretty.ML";
+use "context.ML";
+use "context_position.ML";
 use "Syntax/lexicon.ML";
 use "Syntax/simple_syntax.ML";
-use "context.ML";
 use "sorts.ML";
 use "type.ML";
 use "config.ML";