src/Pure/ML-Systems/poplogml.ML

   fun (x: int) + y = x + y;
   fun (x: int) - y = x - y;
 end;
 
 
+(* bounded time execution *)
+
+(* FIXME proper implementation available? *)
+fun interrupt_timeout time f x =
+  f x;
+
 
 (** interrupts **)      (*Note: may get into race conditions*)
 
 fun ignore_interrupt f x = f x;
 fun raise_interrupt f x = f x;