--- 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];