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