--- a/src/Provers/blast.ML Thu Jul 05 20:01:26 2007 +0200
+++ b/src/Provers/blast.ML Thu Jul 05 20:01:28 2007 +0200
@@ -1247,7 +1247,7 @@
(also prints reconstruction time)
"lim" is depth limit.*)
fun timing_depth_tac start cs lim i st0 =
- let val st = (initialize (theory_of_thm st0); ObjectLogic.atomize_goal i st0);
+ let val st = (initialize (theory_of_thm st0); Conv.gconv_rule ObjectLogic.atomize_prems i st0);
val sign = Thm.theory_of_thm st
val skoprem = fromSubgoal (List.nth(prems_of st, i-1))
val hyps = strip_imp_prems skoprem