diff -r 7acc933bd7cc -r 28b34e8e4a80 src/Pure/ROOT
--- a/src/Pure/ROOT	Sun Apr 06 15:19:22 2014 +0200
+++ b/src/Pure/ROOT	Sun Apr 06 15:38:54 2014 +0200
@@ -6,6 +6,7 @@
     "General/exn.ML"
     "ML-Systems/compiler_polyml.ML"
     "ML-Systems/ml_name_space.ML"
+    "ML-Systems/ml_positions.ML"
     "ML-Systems/ml_pretty.ML"
     "ML-Systems/ml_system.ML"
     "ML-Systems/multithreading.ML"
@@ -30,6 +31,7 @@
     "General/exn.ML"
     "ML-Systems/compiler_polyml.ML"
     "ML-Systems/ml_name_space.ML"
+    "ML-Systems/ml_positions.ML"
     "ML-Systems/ml_pretty.ML"
     "ML-Systems/ml_system.ML"
     "ML-Systems/multithreading.ML"