changeset 71692 | f8e52c0152fe |
parent 69826 | 1bea05713dde |
child 78648 | 852ec09aef13 |
--- a/src/Pure/Concurrent/event_timer.ML Sat Apr 04 21:38:20 2020 +0200 +++ b/src/Pure/Concurrent/event_timer.ML Sun Apr 05 13:05:40 2020 +0200 @@ -130,7 +130,7 @@ fun manager_check manager = if is_some manager andalso Thread.isActive (the manager) then manager else - SOME (Standard_Thread.fork {name = "event_timer", stack_limit = NONE, interrupts = false} + SOME (Isabelle_Thread.fork {name = "event_timer", stack_limit = NONE, interrupts = false} manager_loop); fun shutdown () =