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