| changeset 52738 | 8db0db07bd96 |
| parent 52732 | b4da1f2ec73f |
| child 52761 | 909167fdd367 |
--- a/src/Pure/goal.ML Sat Jul 27 17:34:56 2013 +0200 +++ b/src/Pure/goal.ML Sat Jul 27 20:27:25 2013 +0200 @@ -182,7 +182,7 @@ Inttab.lookup_list (#3 (Synchronized.value forked_proofs)) id; fun stable_futures id = - not (Par_Exn.is_interrupted (Future.join_results (peek_futures id))); + not (Par_Exn.is_interrupted (map_filter Future.peek (peek_futures id))); fun reset_futures () = Synchronized.change_result forked_proofs (fn (_, groups, _) =>