# HG changeset patch
# User wenzelm
# Date 1476716319 -7200
# Node ID 622f4e4ac388938ed2258bac44895253bdc9e873
# Parent  ac2abc987cf9e700f7c4cd03b3816cf83b4e798b
eliminated unused argument;

diff -r ac2abc987cf9 -r 622f4e4ac388 src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Mon Oct 17 15:46:51 2016 +0200
+++ b/src/Pure/Concurrent/future.ML	Mon Oct 17 16:58:39 2016 +0200
@@ -123,10 +123,10 @@
 fun SYNCHRONIZED name = Multithreading.synchronized name lock;
 
 fun wait cond = (*requires SYNCHRONIZED*)
-  Multithreading.sync_wait NONE NONE cond lock;
+  Multithreading.sync_wait NONE cond lock;
 
 fun wait_timeout timeout cond = (*requires SYNCHRONIZED*)
-  Multithreading.sync_wait NONE (SOME (Time.now () + timeout)) cond lock;
+  Multithreading.sync_wait (SOME (Time.now () + timeout)) cond lock;
 
 fun signal cond = (*requires SYNCHRONIZED*)
   ConditionVar.signal cond;
diff -r ac2abc987cf9 -r 622f4e4ac388 src/Pure/Concurrent/multithreading.ML
--- a/src/Pure/Concurrent/multithreading.ML	Mon Oct 17 15:46:51 2016 +0200
+++ b/src/Pure/Concurrent/multithreading.ML	Mon Oct 17 16:58:39 2016 +0200
@@ -9,8 +9,7 @@
   val max_threads: unit -> int
   val max_threads_update: int -> unit
   val enabled: unit -> bool
-  val sync_wait: Thread.threadAttribute list option -> Time.time option ->
-    ConditionVar.conditionVar -> Mutex.mutex -> bool Exn.result
+  val sync_wait: Time.time option -> ConditionVar.conditionVar -> Mutex.mutex -> bool Exn.result
   val trace: int ref
   val tracing: int -> (unit -> string) -> unit
   val tracing_time: bool -> Time.time -> (unit -> string) -> unit
@@ -47,10 +46,9 @@
 
 (* synchronous wait *)
 
-fun sync_wait opt_atts time cond lock =
+fun sync_wait time cond lock =
   Thread_Attributes.with_attributes
-    (Thread_Attributes.sync_interrupts
-      (case opt_atts of SOME atts => atts | NONE => Thread.getAttributes ()))
+    (Thread_Attributes.sync_interrupts (Thread.getAttributes ()))
     (fn _ =>
       (case time of
         SOME t => Exn.Res (ConditionVar.waitUntil (cond, lock, t))
diff -r ac2abc987cf9 -r 622f4e4ac388 src/Pure/Concurrent/single_assignment.ML
--- a/src/Pure/Concurrent/single_assignment.ML	Mon Oct 17 15:46:51 2016 +0200
+++ b/src/Pure/Concurrent/single_assignment.ML	Mon Oct 17 16:58:39 2016 +0200
@@ -37,7 +37,7 @@
       fun wait () =
         (case peek v of
           NONE =>
-            (case Multithreading.sync_wait NONE NONE cond lock of
+            (case Multithreading.sync_wait NONE cond lock of
               Exn.Res _ => wait ()
             | Exn.Exn exn => Exn.reraise exn)
         | SOME x => x);
diff -r ac2abc987cf9 -r 622f4e4ac388 src/Pure/Concurrent/synchronized.ML
--- a/src/Pure/Concurrent/synchronized.ML	Mon Oct 17 15:46:51 2016 +0200
+++ b/src/Pure/Concurrent/synchronized.ML	Mon Oct 17 16:58:39 2016 +0200
@@ -46,7 +46,7 @@
         let val x = ! var in
           (case f x of
             NONE =>
-              (case Multithreading.sync_wait NONE (time_limit x) cond lock of
+              (case Multithreading.sync_wait (time_limit x) cond lock of
                 Exn.Res true => try_change ()
               | Exn.Res false => NONE
               | Exn.Exn exn => Exn.reraise exn)