diff -r 2e427f340ad1 -r 11ae688e4e30 src/Pure/ML-Systems/multithreading_polyml.ML
--- a/src/Pure/ML-Systems/multithreading_polyml.ML	Fri Feb 04 21:52:36 2011 +0100
+++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Sat Feb 05 18:09:57 2011 +0100
@@ -8,7 +8,6 @@
 sig
   val interruptible: ('a -> 'b) -> 'a -> 'b
   val uninterruptible: ((('c -> 'd) -> 'c -> 'd) -> 'a -> 'b) -> 'a -> 'b
-  structure TimeLimit: TIME_LIMIT
 end;
 
 signature BASIC_MULTITHREADING =
@@ -118,29 +117,6 @@
   in time end;
 
 
-(* execution with time limit *)
-
-structure TimeLimit =
-struct
-
-exception TimeOut;
-
-fun timeLimit time f x = uninterruptible (fn restore_attributes => fn () =>
-  let
-    val worker = Thread.self ();
-    val timeout = ref false;
-    val watchdog = Thread.fork (fn () =>
-      (OS.Process.sleep time; timeout := true; Thread.interrupt worker), []);
-
-    val result = Exn.capture (restore_attributes f) x;
-    val was_timeout = Exn.is_interrupt_exn result andalso ! timeout;
-
-    val _ = Thread.interrupt watchdog handle Thread _ => ();
-  in if was_timeout then raise TimeOut else Exn.release result end) ();
-
-end;
-
-
 (* critical section -- may be nested within the same thread *)
 
 local