author | wenzelm |
Mon, 08 Sep 2008 21:08:30 +0200 | |
changeset 28171 | 9b2f9cc9ff4b |
parent 28170 | a18cf8a0e656 |
child 28172 | a46751a649af |
--- a/src/Pure/Concurrent/task_queue.ML Mon Sep 08 20:35:38 2008 +0200 +++ b/src/Pure/Concurrent/task_queue.ML Mon Sep 08 21:08:30 2008 +0200 @@ -20,7 +20,7 @@ val interrupt_task_group: queue -> task -> unit end; -structure TaskQueue (* : TASK_QUEUE *) = +structure TaskQueue: TASK_QUEUE = struct (* identifiers *)