changeset 37852 | a902f158b4fc |
parent 37690 | b16231572c61 |
child 37854 | 047c96f41455 |
--- a/src/Pure/Concurrent/future.ML Tue Jul 20 14:41:13 2010 +0200 +++ b/src/Pure/Concurrent/future.ML Tue Jul 20 14:44:33 2010 +0200 @@ -409,7 +409,7 @@ fun get_result x = (case peek x of - NONE => Exn.Exn (SYS_ERROR "unfinished future") + NONE => Exn.Exn (Fail "Unfinished future") | SOME (exn as Exn.Exn Exn.Interrupt) => (case Exn.flatten_list (Task_Queue.group_status (group_of x)) of [] => exn