--- a/src/Pure/Concurrent/task_queue.ML Wed Apr 06 16:51:52 2016 +0200
+++ b/src/Pure/Concurrent/task_queue.ML Wed Apr 06 17:16:30 2016 +0200
@@ -135,7 +135,7 @@
fun str_of_task_groups task = str_of_task task ^ " in " ^ str_of_groups (group_of_task task);
fun update_timing update (Task {timing, ...}) e =
- uninterruptible (fn restore_attributes => fn () =>
+ Multithreading.uninterruptible (fn restore_attributes => fn () =>
let
val start = Time.now ();
val result = Exn.capture (restore_attributes e) ();