--- a/src/Pure/General/ROOT.ML Wed Aug 06 16:41:40 2008 +0200
+++ b/src/Pure/General/ROOT.ML Thu Aug 07 13:44:33 2008 +0200
@@ -14,6 +14,7 @@
use "symbol.ML";
use "seq.ML";
use "position.ML";
+use "symbol_pos.ML";
use "../ML/ml_lex.ML";
use "../ML/ml_parse.ML";
use "secure.ML";