src/Pure/Thy/thy_info.ML

 fun result_commit (Result {commit, ...}) = commit;
 fun result_ord (Result {weight = i, ...}, Result {weight = j, ...}) = int_ord (j, i);
 
 fun join_theory (Result {theory, id, ...}) =
   Exn.capture Thm.join_theory_proofs theory ::
-  map Exn.Exn (maps Task_Queue.group_status (Goal.peek_futures id));
+  map Exn.Exn (maps Task_Queue.group_status (Execution.peek id));
 
 
 datatype task =
   Task of string list * (theory list -> result) |
   Finished of theory;

     (* FIXME more precise commit order (!?) *)
     val results3 = futures
       |> map (fn future => Exn.capture (fn () => result_commit (Future.join future) ()) ());
 
     (* FIXME avoid global reset_futures (!??) *)
-    val results4 = map Exn.Exn (maps Task_Queue.group_status (Goal.reset_futures ()));
+    val results4 = map Exn.Exn (maps Task_Queue.group_status (Execution.reset ()));
 
     val _ = Par_Exn.release_all (results1 @ results2 @ results3 @ results4);
   in () end);
 
 in