changeset 24688 | a5754ca5c510 |
child 29564 | f8b933a62151 |
--- /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; +