equal
deleted
inserted
replaced
1250 "lim" is depth limit.*) |
1250 "lim" is depth limit.*) |
1251 fun timing_depth_tac start cs lim i st0 = |
1251 fun timing_depth_tac start cs lim i st0 = |
1252 let val thy = Thm.theory_of_thm st0 |
1252 let val thy = Thm.theory_of_thm st0 |
1253 val state = initialize thy |
1253 val state = initialize thy |
1254 val st = Conv.gconv_rule Object_Logic.atomize_prems i st0 |
1254 val st = Conv.gconv_rule Object_Logic.atomize_prems i st0 |
1255 val skoprem = fromSubgoal thy (nth (prems_of st) (i - 1)) |
1255 val skoprem = fromSubgoal thy (Thm.term_of (Thm.cprem_of st i)) |
1256 val hyps = strip_imp_prems skoprem |
1256 val hyps = strip_imp_prems skoprem |
1257 and concl = strip_imp_concl skoprem |
1257 and concl = strip_imp_concl skoprem |
1258 fun cont (tacs,_,choices) = |
1258 fun cont (tacs,_,choices) = |
1259 let val start = Timing.start () |
1259 let val start = Timing.start () |
1260 in |
1260 in |