diff -r aa6a36c730c9 -r 254c324f31fd src/Pure/Concurrent/task_queue.ML
--- a/src/Pure/Concurrent/task_queue.ML	Wed Jul 15 12:43:36 2020 +0200
+++ b/src/Pure/Concurrent/task_queue.ML	Wed Jul 15 16:10:43 2020 +0200
@@ -34,8 +34,7 @@
   val known_task: queue -> task -> bool
   val all_passive: queue -> bool
   val total_jobs: queue -> int
-  val status: queue ->
-    {ready: int, pending: int, running: int, passive: int, urgent: int, total: int}
+  val status: queue -> {ready: int, pending: int, running: int, passive: int, urgent: int}
   val cancel: queue -> group -> Thread.thread list
   val cancel_all: queue -> group list * Thread.thread list
   val finish: task -> queue -> bool * queue
@@ -278,7 +277,7 @@
 
 (* queue status *)
 
-fun status (Queue {jobs, urgent, total, ...}) =
+fun status (Queue {jobs, urgent, ...}) =
   let
     val (x, y, z, w) =
       Task_Graph.fold (fn (_, (job, (deps, _))) => fn (x, y, z, w) =>
@@ -287,7 +286,7 @@
           | Running _ => (x, y, z + 1, w)
           | Passive _ => (x, y, z, w + 1)))
         jobs (0, 0, 0, 0);
-  in {ready = x, pending = y, running = z, passive = w, urgent = urgent, total = total} end;
+  in {ready = x, pending = y, running = z, passive = w, urgent = urgent} end;