diff -r b8efcc9edd7b -r a564458f94db src/HOL/Tools/try0.ML --- a/src/HOL/Tools/try0.ML Sat Mar 05 13:57:25 2016 +0100 +++ b/src/HOL/Tools/try0.ML Sat Mar 05 17:01:45 2016 +0100 @@ -27,7 +27,7 @@ fun can_apply timeout_opt pre post tac st = let val {goal, ...} = Proof.goal st in (case (case timeout_opt of - SOME timeout => TimeLimit.timeLimit timeout + SOME timeout => Timeout.apply timeout | NONE => fn f => fn x => f x) (Seq.pull o tac) (pre st) of SOME (x, _) => Thm.nprems_of (post x) < Thm.nprems_of goal | NONE => false)