src/HOL/Tools/try0.ML
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)