src/Pure/ML-Systems/mlworks.ML

--- a/src/Pure/ML-Systems/mlworks.ML	Tue Jun 01 00:18:01 2004 +0200
+++ b/src/Pure/ML-Systems/mlworks.ML	Tue Jun 01 00:26:13 2004 +0200
@@ -59,6 +59,18 @@
 
 use "ML-Systems/cpu-timer-gc.ML"
 
+(* bounded time execution *)
+
+(* FIXME proper implementation available? *)
+
+structure TimeLimit : sig
+   exception TimeOut
+   val timeLimit : Time.time -> ('a -> 'b) -> 'a -> 'b
+end = struct
+   exception TimeOut
+   fun timeLimit t f x =
+      f x;
+end;
 
 (* ML command execution *)