--- a/src/Pure/ROOT Wed Feb 17 23:29:35 2016 +0100
+++ b/src/Pure/ROOT Thu Feb 18 23:10:28 2016 +0100
@@ -25,7 +25,6 @@
"RAW/ml_stack_polyml-5.6.ML"
"RAW/ml_system.ML"
"RAW/multithreading.ML"
- "RAW/multithreading_polyml.ML"
"RAW/share_common_data_polyml-5.3.0.ML"
"RAW/single_assignment_polyml.ML"
"RAW/unsynchronized.ML"
@@ -57,7 +56,6 @@
"RAW/ml_stack_polyml-5.6.ML"
"RAW/ml_system.ML"
"RAW/multithreading.ML"
- "RAW/multithreading_polyml.ML"
"RAW/share_common_data_polyml-5.3.0.ML"
"RAW/single_assignment_polyml.ML"
"RAW/unsynchronized.ML"
@@ -65,24 +63,19 @@
"RAW/windows_path.ML"
"Concurrent/bash.ML"
- "Concurrent/bash_sequential.ML"
"Concurrent/bash_windows.ML"
"Concurrent/cache.ML"
"Concurrent/counter.ML"
"Concurrent/event_timer.ML"
"Concurrent/future.ML"
"Concurrent/lazy.ML"
- "Concurrent/lazy_sequential.ML"
"Concurrent/mailbox.ML"
"Concurrent/par_exn.ML"
"Concurrent/par_list.ML"
- "Concurrent/par_list_sequential.ML"
"Concurrent/random.ML"
"Concurrent/single_assignment.ML"
- "Concurrent/single_assignment_sequential.ML"
"Concurrent/standard_thread.ML"
"Concurrent/synchronized.ML"
- "Concurrent/synchronized_sequential.ML"
"Concurrent/task_queue.ML"
"Concurrent/time_limit.ML"
"General/alist.ML"