1.1 --- a/src/Pure/Concurrent/future.ML Fri Jan 18 23:33:17 2013 +0100
1.2 +++ b/src/Pure/Concurrent/future.ML Sat Jan 19 00:00:29 2013 +0100
1.3 @@ -61,7 +61,6 @@
1.4 type params = {name: string, group: group option, deps: task list, pri: int, interrupts: bool}
1.5 val default_params: params
1.6 val forks: params -> (unit -> 'a) list -> 'a future list
1.7 - val fork_pri: int -> (unit -> 'a) -> 'a future
1.8 val fork: (unit -> 'a) -> 'a future
1.9 val join_results: 'a future list -> 'a Exn.result list
1.10 val join_result: 'a future -> 'a Exn.result
1.11 @@ -521,10 +520,8 @@
1.12 in futures end)
1.13 end;
1.14
1.15 -fun fork_pri pri e =
1.16 - (singleton o forks) {name = "fork", group = NONE, deps = [], pri = pri, interrupts = true} e;
1.17 -
1.18 -fun fork e = fork_pri 0 e;
1.19 +fun fork e =
1.20 + (singleton o forks) {name = "fork", group = NONE, deps = [], pri = 0, interrupts = true} e;
1.21
1.22
1.23 (* join *)