clarified raw_blast, which is not really a tactic since it operates directly on subgoal 1 without bounds check (cf. c46107e6714b);
uniform handling of exceptions in depth_tac and blast_tac, discontinued separate blast_depth_tac;
tuned blast_tac: atomize prems only once, outside DEEPEN;

--- a/src/Provers/blast.ML	Thu Jun 09 20:56:08 2011 +0200
+++ b/src/Provers/blast.ML	Thu Jun 09 22:13:21 2011 +0200
@@ -1234,18 +1234,14 @@
   in  skoSubgoal 0 (from 0 (discard_foralls t))  end;
 
 
-(*Tactic using tableau engine and proof reconstruction.
- "start" is CPU time at start, for printing SEARCH time
-        (also prints reconstruction time)
+(*Tableau engine and proof reconstruction operating on subgoal 1.
+ "start" is CPU time at start, for printing SEARCH time (also prints reconstruction time)
  "lim" is depth limit.*)
-fun timing_depth_tac start ctxt lim i st0 =
+fun raw_blast start ctxt lim st =
   let val thy = Proof_Context.theory_of ctxt
       val state = initialize ctxt
       val trace = Config.get ctxt trace;
       val stats = Config.get ctxt stats;
-      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
@@ -1265,20 +1261,29 @@
           end
   in
     prove (state, start, [initBranch (mkGoal concl :: hyps, lim)], cont)
-    |> Seq.map (rotate_prems (1 - i))
   end
-  handle PROVE => Seq.empty | THM _ => Seq.empty;
+  handle PROVE => Seq.empty
+    | TRANS s => (if Config.get ctxt trace then warning ("Blast: " ^ s) else (); Seq.empty);
 
-(*Public version with fixed depth*)
-fun depth_tac ctxt lim i st = timing_depth_tac (Timing.start ()) ctxt lim i st;
+fun depth_tac ctxt lim i st =
+  SELECT_GOAL
+    (Object_Logic.atomize_prems_tac 1 THEN
+      raw_blast (Timing.start ()) ctxt lim) i st;
+
 
 val (depth_limit, setup_depth_limit) =
   Attrib.config_int @{binding blast_depth_limit} (K 20);
 
 fun blast_tac ctxt i st =
-  ((DEEPEN (1, Config.get ctxt depth_limit) (timing_depth_tac (Timing.start ()) ctxt) 0) i
-    THEN flexflex_tac) st
-  handle TRANS s => (if Config.get ctxt trace then warning ("blast: " ^ s) else (); Seq.empty);
+  let
+    val start = Timing.start ();
+    val lim = Config.get ctxt depth_limit;
+  in
+    SELECT_GOAL
+     (Object_Logic.atomize_prems_tac 1 THEN
+      DEEPEN (1, lim) (fn m => fn _ => raw_blast start ctxt m) 0 1 THEN
+      flexflex_tac) i st
+  end;
 
 
 

--- a/src/Provers/clasimp.ML	Thu Jun 09 20:56:08 2011 +0200
+++ b/src/Provers/clasimp.ML	Thu Jun 09 22:13:21 2011 +0200
@@ -117,10 +117,6 @@
 
 (* auto_tac *)
 
-fun blast_depth_tac ctxt m i thm =
-  Blast.depth_tac ctxt m i thm
-    handle Blast.TRANS s => (warning ("Blast_tac: " ^ s); Seq.empty);
-
 (* a variant of depth_tac that avoids interference of the simplifier
    with dup_step_tac when they are combined by auto_tac *)
 local
@@ -140,12 +136,12 @@
 
 end;
 
-(*Designed to be idempotent, except if blast_depth_tac instantiates variables
+(*Designed to be idempotent, except if Blast.depth_tac instantiates variables
   in some of the subgoals*)
 fun mk_auto_tac ctxt m n =
   let
     val main_tac =
-      blast_depth_tac ctxt m  (* fast but can't use wrappers *)
+      Blast.depth_tac ctxt m  (* fast but can't use wrappers *)
       ORELSE'
       (CHANGED o nodup_depth_tac (addss ctxt) n);  (* slower but more general *)
   in