# HG changeset patch
# User wenzelm
# Date 1314114186 -7200
# Node ID c4a86d72a5cc2c36e450b0cd1d167cbf4cd2f7d2
# Parent  8d6869a8d4ec7a4551b12077ce9261749e2b9ed2
tuned signature;

diff -r 8d6869a8d4ec -r c4a86d72a5cc src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Tue Aug 23 17:12:54 2011 +0200
+++ b/src/Pure/Concurrent/future.ML	Tue Aug 23 17:43:06 2011 +0200
@@ -54,10 +54,9 @@
   val interruptible_task: ('a -> 'b) -> 'a -> 'b
   val cancel_group: group -> task list
   val cancel: 'a future -> task list
-  type fork_params =
-    {name: string, group: group option, deps: task list, pri: int, interrupts: bool}
-  val default_params: fork_params
-  val forks: fork_params -> (unit -> 'a) list -> 'a future list
+  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
@@ -67,7 +66,7 @@
   val join_tasks: task list -> unit
   val value_result: 'a Exn.result -> 'a future
   val value: 'a -> 'a future
-  val cond_forks: fork_params -> (unit -> 'a) list -> 'a future list
+  val cond_forks: params -> (unit -> 'a) list -> 'a future list
   val map: ('a -> 'b) -> 'a future -> 'b future
   val promise_group: group -> (unit -> unit) -> 'a future
   val promise: (unit -> unit) -> 'a future
@@ -459,13 +458,10 @@
 
 (* fork *)
 
-type fork_params =
-  {name: string, group: group option, deps: task list, pri: int, interrupts: bool};
+type params = {name: string, group: group option, deps: task list, pri: int, interrupts: bool};
+val default_params: params = {name = "", group = NONE, deps = [], pri = 0, interrupts = true};
 
-val default_params: fork_params =
-  {name = "", group = NONE, deps = [], pri = 0, interrupts = true};
-
-fun forks ({name, group, deps, pri, interrupts}: fork_params) es =
+fun forks ({name, group, deps, pri, interrupts}: params) es =
   if null es then []
   else
     let
diff -r 8d6869a8d4ec -r c4a86d72a5cc src/Pure/Concurrent/lazy.ML
--- a/src/Pure/Concurrent/lazy.ML	Tue Aug 23 17:12:54 2011 +0200
+++ b/src/Pure/Concurrent/lazy.ML	Tue Aug 23 17:43:06 2011 +0200
@@ -16,7 +16,7 @@
   val force_result: 'a lazy -> 'a Exn.result
   val force: 'a lazy -> 'a
   val map: ('a -> 'b) -> 'a lazy -> 'b lazy
-  val future: Future.fork_params -> 'a lazy -> 'a future
+  val future: Future.params -> 'a lazy -> 'a future
 end;
 
 structure Lazy: LAZY =