src/Provers/blast.ML

  "lim" is depth limit.*)
 fun timing_depth_tac start cs lim i st0 =
   let val thy = Thm.theory_of_thm st0
       val state = initialize thy
       val st = Conv.gconv_rule Object_Logic.atomize_prems i st0
-      val skoprem = fromSubgoal thy (nth (prems_of st) (i - 1))
+      val skoprem = fromSubgoal thy (Thm.term_of (Thm.cprem_of st i))
       val hyps  = strip_imp_prems skoprem
       and concl = strip_imp_concl skoprem
       fun cont (tacs,_,choices) =
           let val start = Timing.start ()
           in