--- a/src/HOL/TPTP/atp_problem_import.ML Sat Mar 05 13:57:25 2016 +0100
+++ b/src/HOL/TPTP/atp_problem_import.ML Sat Mar 05 17:01:45 2016 +0100
@@ -137,10 +137,8 @@
let
val _ = writeln ("running " ^ name ^ " for " ^ string_of_int seconds ^ " s")
val result =
- TimeLimit.timeLimit (Time.fromSeconds seconds) (fn () => SINGLE (SOLVE tac) st) ()
- handle
- TimeLimit.TimeOut => NONE
- | ERROR _ => NONE
+ Timeout.apply (Time.fromSeconds seconds) (fn () => SINGLE (SOLVE tac) st) ()
+ handle Timeout.TIMEOUT _ => NONE | ERROR _ => NONE
in
(case result of
NONE => (writeln ("FAILURE: " ^ name); Seq.empty)