# HG changeset patch
# User wenzelm
# Date 1220898809 -7200
# Node ID 356fc873474136bbb116522d8d77765c25dec6ef
# Parent  ba410235ff04a0fe278ffbe53a65eaa1a2985c6a
removed unused sync_interrupts;

diff -r ba410235ff04 -r 356fc8734741 src/Pure/ML-Systems/multithreading.ML
--- a/src/Pure/ML-Systems/multithreading.ML	Mon Sep 08 20:33:27 2008 +0200
+++ b/src/Pure/ML-Systems/multithreading.ML	Mon Sep 08 20:33:29 2008 +0200
@@ -20,7 +20,6 @@
   val max_threads: int ref
   val max_threads_value: unit -> int
   val no_interrupts: Thread.threadAttribute list
-  val sync_interrupts: Thread.threadAttribute list
   val regular_interrupts: Thread.threadAttribute list
   val with_attributes: Thread.threadAttribute list ->
     (Thread.threadAttribute list -> 'a -> 'b) -> 'a -> 'b
@@ -41,7 +40,6 @@
 fun max_threads_value () = Int.max (! max_threads, 1);
 
 val no_interrupts = [];
-val sync_interrupts = [];
 val regular_interrupts = [];
 
 fun with_attributes _ f x = f [] x;
diff -r ba410235ff04 -r 356fc8734741 src/Pure/ML-Systems/multithreading_polyml.ML
--- a/src/Pure/ML-Systems/multithreading_polyml.ML	Mon Sep 08 20:33:27 2008 +0200
+++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Mon Sep 08 20:33:29 2008 +0200
@@ -65,9 +65,6 @@
 val no_interrupts =
   [Thread.EnableBroadcastInterrupt false, Thread.InterruptState Thread.InterruptDefer];
 
-val sync_interrupts =
-  [Thread.EnableBroadcastInterrupt false, Thread.InterruptState Thread.InterruptSynch];
-
 val regular_interrupts =
   [Thread.EnableBroadcastInterrupt true, Thread.InterruptState Thread.InterruptAsynchOnce];