diff -r b8efcc9edd7b -r a564458f94db src/Tools/quickcheck.ML --- a/src/Tools/quickcheck.ML Sat Mar 05 13:57:25 2016 +0100 +++ b/src/Tools/quickcheck.ML Sat Mar 05 17:01:45 2016 +0100 @@ -282,9 +282,9 @@ fun limit timeout (limit_time, is_interactive) f exc () = if limit_time then - TimeLimit.timeLimit timeout f () - handle TimeLimit.TimeOut => - if is_interactive then exc () else raise TimeLimit.TimeOut + Timeout.apply timeout f () + handle timeout_exn as Timeout.TIMEOUT _ => + if is_interactive then exc () else Exn.reraise timeout_exn else f (); fun message ctxt s = if Config.get ctxt quiet then () else writeln s;