src/Pure/ML-Systems/poplogml.ML
changeset 18760 97aaecb84afe
parent 18392 fdefc3cd45c5
child 21295 63552bc99cfb
--- a/src/Pure/ML-Systems/poplogml.ML	Mon Jan 23 15:23:31 2006 +0100
+++ b/src/Pure/ML-Systems/poplogml.ML	Mon Jan 23 17:29:52 2006 +0100
@@ -269,6 +269,12 @@
 end;
 
 
+(* bounded time execution *)
+
+(* FIXME proper implementation available? *)
+fun interrupt_timeout time f x =
+  f x;
+
 
 (** interrupts **)      (*Note: may get into race conditions*)