--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML-Systems/time_limit.ML	Mon Sep 24 13:52:50 2007 +0200
@@ -0,0 +1,21 @@
+(*  Title:      Pure/ML-Systems/time_limit.ML
+    ID:         $Id$
+    Author:     Makarius
+
+Dummy implementation of NJ's TimeLimit structure.
+*)
+
+signature TIME_LIMIT =
+sig
+  exception TimeOut
+  val timeLimit : Time.time -> ('a -> 'b) -> 'a -> 'b
+end;
+
+structure TimeLimit: TIME_LIMIT =
+struct
+
+exception TimeOut;
+fun timeLimit _ f x = f x;
+
+end;
+