src/Pure/ROOT

--- a/src/Pure/ROOT	Thu Jul 16 11:38:18 2015 +0200
+++ b/src/Pure/ROOT	Thu Jul 16 14:40:23 2015 +0200
@@ -9,20 +9,22 @@
     "ML-Systems/ml_debugger_dummy.ML"
     "ML-Systems/ml_debugger_polyml-5.5.3.ML"
     "ML-Systems/ml_name_space.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_system.ML"
     "ML-Systems/multithreading.ML"
     "ML-Systems/multithreading_polyml.ML"
     "ML-Systems/overloading_smlnj.ML"
-    "ML-Systems/polyml.ML"
     "ML-Systems/polyml-5.5.2.ML"
     "ML-Systems/polyml-5.5.3.ML"
+    "ML-Systems/polyml.ML"
     "ML-Systems/pp_dummy.ML"
     "ML-Systems/proper_int.ML"
+    "ML-Systems/share_common_data_polyml-5.3.0.ML"
     "ML-Systems/single_assignment.ML"
     "ML-Systems/single_assignment_polyml.ML"
-    "ML-Systems/share_common_data_polyml-5.3.0.ML"
     "ML-Systems/smlnj.ML"
     "ML-Systems/thread_dummy.ML"
     "ML-Systems/universal.ML"
@@ -35,18 +37,23 @@
     "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_debugger_polyml-5.5.3.ML"
     "ML-Systems/ml_name_space.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_system.ML"
     "ML-Systems/multithreading.ML"
     "ML-Systems/multithreading_polyml.ML"
     "ML-Systems/overloading_smlnj.ML"
-    "ML-Systems/polyml.ML"
     "ML-Systems/polyml-5.5.2.ML"
     "ML-Systems/polyml-5.5.3.ML"
+    "ML-Systems/polyml.ML"
     "ML-Systems/pp_dummy.ML"
     "ML-Systems/proper_int.ML"
+    "ML-Systems/share_common_data_polyml-5.3.0.ML"
     "ML-Systems/single_assignment.ML"
     "ML-Systems/single_assignment_polyml.ML"
     "ML-Systems/smlnj.ML"