diff -r e27cfd2bf094 -r 0d4ee4168e41 src/Pure/ROOT --- a/src/Pure/ROOT Tue Nov 03 11:24:42 2015 +0100 +++ b/src/Pure/ROOT Tue Nov 03 13:54:34 2015 +0100 @@ -86,9 +86,9 @@ "Concurrent/par_list.ML" "Concurrent/par_list_sequential.ML" "Concurrent/random.ML" - "Concurrent/simple_thread.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"