--- a/src/Pure/Thy/thy_info.ML Wed Oct 08 20:21:34 2008 +0200
+++ b/src/Pure/Thy/thy_info.ML Wed Oct 08 20:21:35 2008 +0200
@@ -326,12 +326,7 @@
val deps = map_filter (Symtab.lookup tab) (Graph.imm_preds task_graph name);
val x = Future.future (SOME group) deps true body;
in (x, Symtab.update (name, Future.task_of x) tab) end;
- in
- #1 (fold_map future tasks Symtab.empty)
- |> uninterruptible (fn _ => Future.join_results)
- |> Exn.release_all
- |> ignore
- end;
+ in ignore (Exn.release_all (Future.join_results (#1 (fold_map future tasks Symtab.empty)))) end;
local