src/Pure/ML-Systems/smlnj-interrupt-timeout.ML

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML-Systems/smlnj-interrupt-timeout.ML	Mon Jan 23 17:29:52 2006 +0100
@@ -0,0 +1,11 @@
+(*  Title:      Pure/ML-Systems/smlnj-interrupt-timeout.ML
+    ID:         $Id$
+    Author:     Tjark Weber, Makarius
+    Copyright   2006
+
+Bounded time execution (similar to SML/NJ's TimeLimit structure).
+*)
+
+fun interrupt_timeout time f x =
+  TimeLimit.timeLimit time f x
+    handle TimeLimit.TimeOut => raise SML90.Interrupt;