| changeset 62519 | a564458f94db |
| parent 61877 | 276ad4354069 |
| child 62969 | 9f394a16c557 |
--- 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)