diff -r 16c6ae7d1aa6 -r 4e2417eb603e src/Pure/Thy/thy_info.ML
--- 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