--- a/src/Pure/goal.ML Mon Jul 29 13:00:36 2013 +0200
+++ b/src/Pure/goal.ML Mon Jul 29 13:24:15 2013 +0200
@@ -27,7 +27,6 @@
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 stable_futures: int-> bool
val reset_futures: unit -> Future.group list
val shutdown_futures: unit -> unit
val skip_proofs_enabled: unit -> bool
@@ -181,9 +180,6 @@
fun peek_futures id =
Inttab.lookup_list (#3 (Synchronized.value forked_proofs)) id;
-fun stable_futures id =
- not (Par_Exn.is_interrupted (map_filter Future.peek (peek_futures id)));
-
fun reset_futures () =
Synchronized.change_result forked_proofs (fn (_, groups, _) =>
(Future.forked_proofs := 0; (groups, (0, [], Inttab.empty))));