# [isabelle] Using timeLimit with tactics

Hi all,
I'm trying to limit the running time of tactics under Isabelle 2011-1, using
timeLimit. Both of the following examples work as I want them to:
ML_prf {*
fun loop_tac ctxt i = loop_tac ctxt i
*}
apply(tactic {*
TimeLimit.timeLimit (Time.fromMilliseconds 500) (loop_tac @{context}) 1
*})
apply(tactic {*
TimeLimit.timeLimit (Time.fromMilliseconds 50) ((auto_tac @{context}))
*}) [1]
i.e. they timeout after the appropriate time. However neither of the following
do anything:
apply(tactic {*
TimeLimit.timeLimit (Time.fromMilliseconds 500) loop_tac @{context} 1
*})
apply(tactic {*
TimeLimit.timeLimit (Time.fromMilliseconds 500) (auto_tac @{context})
*}) [1]
The difference is the grouping of the arguments in the first example (hence
changing the type of timeLimit's result), and increasing the limit in the
second example. I can't really make any sense of it. Can anyone shed some
light on this for me? Or point me to some working examples?
Thanks,
Ognjen

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*