--- 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"