tuned signature;
authorwenzelm
Sat, 19 Jan 2013 00:00:29 +0100
changeset 519981290afb88f90
parent 51997 a7aa17a1f721
child 51999 7c07ade3c8e0
tuned signature;
src/Pure/Concurrent/future.ML
     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 *)