--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Concurrent/time_limit_dummy.ML	Sat Feb 05 18:09:57 2011 +0100
@@ -0,0 +1,15 @@
+(*  Title:      Pure/Concurrent/time_limit_dummy.ML
+    Author:     Makarius
+
+Execution with time limit -- dummy version.
+*)
+
+structure TimeLimit: TIME_LIMIT =
+struct
+
+exception TimeOut;
+
+fun timeLimit _ f x = (warning "No timeout support on this ML platform"; f x);
+
+end;
+