changeset 61556 | 0d4ee4168e41 |
parent 61441 | 20ff1d5c74e1 |
child 61619 | f22054b192b0 |
--- 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"