diff -r dc13552494a2 -r 260949bf6529 src/Pure/goal.ML
--- a/src/Pure/goal.ML	Mon Jul 29 13:43:43 2013 +0200
+++ b/src/Pure/goal.ML	Mon Jul 29 14:18:57 2013 +0200
@@ -27,6 +27,7 @@
   val fork_params: {name: string, pos: Position.T, pri: int} -> (unit -> 'a) -> 'a future
   val fork: int -> (unit -> 'a) -> 'a future
   val peek_futures: int -> unit future list
+  val purge_futures: int list -> unit
   val reset_futures: unit -> Future.group list
   val shutdown_futures: unit -> unit
   val skip_proofs_enabled: unit -> bool
@@ -180,6 +181,14 @@
 fun peek_futures id =
   map #2 (Inttab.lookup_list (#2 (Synchronized.value forked_proofs)) id);
 
+fun purge_futures ids =
+  Synchronized.change forked_proofs (fn (_, tab) =>
+    let
+      val tab' = fold Inttab.delete_safe ids tab;
+      val n' = Inttab.fold (Integer.add o length o #2) tab' 0;
+      val _ = Future.forked_proofs := n';
+    in (n', tab') end);
+
 fun reset_futures () =
   Synchronized.change_result forked_proofs (fn (_, tab) =>
     let