diff -r e27cfd2bf094 -r 0d4ee4168e41 src/Pure/Concurrent/event_timer.ML --- 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 () =