# HG changeset patch
# User wenzelm
# Date 1302983147 -7200
# Node ID 167e8ba0f4b1a9281e030e3b763cee79c53e2072
# Parent  3b8498ac231412d67cf0a8f5093ba25d56d88ea6
tuned blast: navigate to subgoal only once;

diff -r 3b8498ac2314 -r 167e8ba0f4b1 src/Provers/blast.ML
--- a/src/Provers/blast.ML	Sat Apr 16 20:49:48 2011 +0200
+++ b/src/Provers/blast.ML	Sat Apr 16 21:45:47 2011 +0200
@@ -1251,14 +1251,16 @@
 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 (Thm.term_of (Thm.cprem_of st i))
+      val st = st0
+        |> rotate_prems (i - 1)
+        |> Conv.gconv_rule Object_Logic.atomize_prems 1
+      val skoprem = fromSubgoal thy (#1 (Logic.dest_implies (Thm.prop_of st)))
       val hyps  = strip_imp_prems skoprem
       and concl = strip_imp_concl skoprem
       fun cont (tacs,_,choices) =
           let val start = Timing.start ()
           in
-          case Seq.pull(EVERY' (rev tacs) i st) of
+          case Seq.pull(EVERY' (rev tacs) 1 st) of
               NONE => (writeln ("PROOF FAILED for depth " ^
                                 string_of_int lim);
                        if !trace then error "************************\n"
@@ -1269,8 +1271,11 @@
                        else ();
                        Seq.make(fn()=> cell))
           end
-  in prove (state, start, cs, [initBranch (mkGoal concl :: hyps, lim)], cont) end
-  handle PROVE     => Seq.empty
+  in
+    prove (state, start, cs, [initBranch (mkGoal concl :: hyps, lim)], cont)
+    |> Seq.map (rotate_prems (1 - i))
+  end
+  handle PROVE => Seq.empty;
 
 (*Public version with fixed depth*)
 fun depth_tac cs lim i st = timing_depth_tac (Timing.start ()) cs lim i st;