| changeset 32592 | e29c0b7dcf66 |
| parent 32420 | 6473d1952023 |
| child 32616 | 8ef1aa1cfcc7 |
--- a/src/Pure/Concurrent/future.ML Wed Sep 16 21:31:57 2009 +0200 +++ b/src/Pure/Concurrent/future.ML Wed Sep 16 22:46:10 2009 +0200 @@ -84,7 +84,7 @@ fun group_of (Future {group, ...}) = group; fun result_of (Future {result, ...}) = result; -fun peek x = Synchronized.peek (result_of x); +fun peek x = Synchronized.value (result_of x); fun is_finished x = is_some (peek x); fun value x = Future