--- a/src/Pure/Concurrent/future.ML Fri Jan 18 23:33:17 2013 +0100
+++ b/src/Pure/Concurrent/future.ML Sat Jan 19 00:00:29 2013 +0100
@@ -61,7 +61,6 @@
type params = {name: string, group: group option, deps: task list, pri: int, interrupts: bool}
val default_params: params
val forks: params -> (unit -> 'a) list -> 'a future list
- val fork_pri: int -> (unit -> 'a) -> 'a future
val fork: (unit -> 'a) -> 'a future
val join_results: 'a future list -> 'a Exn.result list
val join_result: 'a future -> 'a Exn.result
@@ -521,10 +520,8 @@
in futures end)
end;
-fun fork_pri pri e =
- (singleton o forks) {name = "fork", group = NONE, deps = [], pri = pri, interrupts = true} e;
-
-fun fork e = fork_pri 0 e;
+fun fork e =
+ (singleton o forks) {name = "fork", group = NONE, deps = [], pri = 0, interrupts = true} e;
(* join *)