diff -r 4eba53a0ac3d -r d86b4cd0f1ec src/Pure/ROOT
--- a/src/Pure/ROOT	Fri Jul 17 16:23:25 2015 +0200
+++ b/src/Pure/ROOT	Fri Jul 17 16:43:53 2015 +0200
@@ -6,7 +6,9 @@
     "General/exn.ML"
     "ML-Systems/compiler_polyml.ML"
     "ML-Systems/exn_trace_polyml-5.5.1.ML"
-    "ML-Systems/ml_debugger_dummy.ML"
+    "ML-Systems/ml_compiler_parameters.ML"
+    "ML-Systems/ml_compiler_parameters_polyml-5.5.3.ML"
+    "ML-Systems/ml_debugger.ML"
     "ML-Systems/ml_debugger_polyml-5.5.3.ML"
     "ML-Systems/ml_name_space.ML"
     "ML-Systems/ml_parse_tree.ML"
@@ -37,7 +39,9 @@
     "General/exn.ML"
     "ML-Systems/compiler_polyml.ML"
     "ML-Systems/exn_trace_polyml-5.5.1.ML"
-    "ML-Systems/ml_debugger_dummy.ML"
+    "ML-Systems/ml_compiler_parameters.ML"
+    "ML-Systems/ml_compiler_parameters_polyml-5.5.3.ML"
+    "ML-Systems/ml_debugger.ML"
     "ML-Systems/ml_debugger_polyml-5.5.3.ML"
     "ML-Systems/ml_name_space.ML"
     "ML-Systems/ml_parse_tree.ML"