changeset 61556 | 0d4ee4168e41 |
parent 60764 | b610ba36e02c |
child 62239 | 6ee95b93fbed |
--- a/src/Pure/Concurrent/event_timer.ML Tue Nov 03 11:24:42 2015 +0100 +++ b/src/Pure/Concurrent/event_timer.ML Tue Nov 03 13:54:34 2015 +0100 @@ -105,7 +105,7 @@ fun manager_check manager = if is_some manager andalso Thread.isActive (the manager) then manager else - SOME (Simple_Thread.fork {name = "event_timer", stack_limit = NONE, interrupts = false} + SOME (Standard_Thread.fork {name = "event_timer", stack_limit = NONE, interrupts = false} manager_loop); fun shutdown () =