--- a/src/Pure/ROOT Fri Nov 20 15:54:46 2015 +0000
+++ b/src/Pure/ROOT Fri Nov 20 21:52:05 2015 +0100
@@ -11,10 +11,14 @@
"ML-Systems/ml_debugger.ML"
"ML-Systems/ml_debugger_polyml-5.5.3.ML"
"ML-Systems/ml_name_space.ML"
+ "ML-Systems/ml_name_space_polyml-5.6.ML"
+ "ML-Systems/ml_name_space_polyml.ML"
"ML-Systems/ml_parse_tree.ML"
"ML-Systems/ml_parse_tree_polyml-5.5.3.ML"
"ML-Systems/ml_positions.ML"
"ML-Systems/ml_pretty.ML"
+ "ML-Systems/ml_profiling_polyml-5.6.ML"
+ "ML-Systems/ml_profiling_polyml.ML"
"ML-Systems/ml_stack_dummy.ML"
"ML-Systems/ml_stack_polyml-5.5.3.ML"
"ML-Systems/ml_system.ML"
@@ -23,6 +27,7 @@
"ML-Systems/overloading_smlnj.ML"
"ML-Systems/polyml-5.5.2.ML"
"ML-Systems/polyml-5.5.3.ML"
+ "ML-Systems/polyml-5.6.ML"
"ML-Systems/polyml.ML"
"ML-Systems/pp_dummy.ML"
"ML-Systems/proper_int.ML"
@@ -47,10 +52,14 @@
"ML-Systems/ml_debugger.ML"
"ML-Systems/ml_debugger_polyml-5.5.3.ML"
"ML-Systems/ml_name_space.ML"
+ "ML-Systems/ml_name_space_polyml-5.6.ML"
+ "ML-Systems/ml_name_space_polyml.ML"
"ML-Systems/ml_parse_tree.ML"
"ML-Systems/ml_parse_tree_polyml-5.5.3.ML"
"ML-Systems/ml_positions.ML"
"ML-Systems/ml_pretty.ML"
+ "ML-Systems/ml_profiling_polyml-5.6.ML"
+ "ML-Systems/ml_profiling_polyml.ML"
"ML-Systems/ml_stack_dummy.ML"
"ML-Systems/ml_stack_polyml-5.5.3.ML"
"ML-Systems/ml_system.ML"
@@ -59,6 +68,7 @@
"ML-Systems/overloading_smlnj.ML"
"ML-Systems/polyml-5.5.2.ML"
"ML-Systems/polyml-5.5.3.ML"
+ "ML-Systems/polyml-5.6.ML"
"ML-Systems/polyml.ML"
"ML-Systems/pp_dummy.ML"
"ML-Systems/proper_int.ML"