# HG changeset patch
# User wenzelm
# Date 1358550029 -3600
# Node ID 1290afb88f903f8ef49e24615412a72340f4f497
# Parent  a7aa17a1f721284794128e5c3e157006db908be9
tuned signature;

diff -r a7aa17a1f721 -r 1290afb88f90 src/Pure/Concurrent/future.ML
--- 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 *)