| author | wenzelm |
| Fri, 15 Aug 2008 21:57:22 +0200 | |
| changeset 27903 | af1b39debf30 |
| parent 24688 | a5754ca5c510 |
| child 29564 | f8b933a62151 |
| permissions | -rw-r--r-- |
(* 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;