future_schedule: uninterruptible join;

--- a/src/Pure/Thy/thy_info.ML	Wed Sep 10 21:50:32 2008 +0200
+++ b/src/Pure/Thy/thy_info.ML	Wed Sep 10 22:29:36 2008 +0200
@@ -331,7 +331,7 @@
       in (x, Symtab.update (name, Future.task_of x) tab) end;
 
     val exns = #1 (fold_map future tasks Symtab.empty)
-      |> Future.join_results
+      |> uninterruptible (fn _ => Future.join_results)
       |> map_filter Exn.get_exn;
   in
     if null exns then ()