src/Pure/ROOT
changeset 60908 d32915a03c63
parent 60745 d86b4cd0f1ec
child 60923 020becec359c
--- a/src/Pure/ROOT	Tue Aug 11 22:11:09 2015 +0200
+++ b/src/Pure/ROOT	Tue Aug 11 22:17:19 2015 +0200
@@ -6,6 +6,8 @@
     "General/exn.ML"
     "ML-Systems/compiler_polyml.ML"
     "ML-Systems/exn_trace_polyml-5.5.1.ML"
+    "ML-Systems/maximum_ml_stack_dummy.ML"
+    "ML-Systems/maximum_ml_stack_polyml-5.5.3.ML"
     "ML-Systems/ml_compiler_parameters.ML"
     "ML-Systems/ml_compiler_parameters_polyml-5.5.3.ML"
     "ML-Systems/ml_debugger.ML"
@@ -39,6 +41,8 @@
     "General/exn.ML"
     "ML-Systems/compiler_polyml.ML"
     "ML-Systems/exn_trace_polyml-5.5.1.ML"
+    "ML-Systems/maximum_ml_stack_dummy.ML"
+    "ML-Systems/maximum_ml_stack_polyml-5.5.3.ML"
     "ML-Systems/ml_compiler_parameters.ML"
     "ML-Systems/ml_compiler_parameters_polyml-5.5.3.ML"
     "ML-Systems/ml_debugger.ML"
@@ -69,6 +73,7 @@
     "Concurrent/bash.ML"
     "Concurrent/bash_sequential.ML"
     "Concurrent/cache.ML"
+    "Concurrent/counter.ML"
     "Concurrent/event_timer.ML"
     "Concurrent/future.ML"
     "Concurrent/lazy.ML"
@@ -174,8 +179,8 @@
     "ML/ml_env.ML"
     "ML/ml_file.ML"
     "ML/ml_lex.ML"
+    "ML/ml_options.ML"
     "ML/ml_parse.ML"
-    "ML/ml_options.ML"
     "ML/ml_statistics_dummy.ML"
     "ML/ml_statistics_polyml-5.5.0.ML"
     "ML/ml_syntax.ML"
@@ -281,4 +286,3 @@
     "type_infer_context.ML"
     "unify.ML"
     "variable.ML"
-