diff -r f18cf88453d6 -r 3e153e719039 src/Provers/blast.ML
--- a/src/Provers/blast.ML	Fri Jun 10 11:47:52 2011 +0200
+++ b/src/Provers/blast.ML	Fri Jun 10 12:51:29 2011 +0200
@@ -1262,6 +1262,7 @@
           end
   in
     prove (state, start, [initBranch (mkGoal concl :: hyps, lim)], cont)
+    |> Seq.maps Thm.flexflex_rule
   end
   handle PROVE => Seq.empty
     | TRANS s => (if Config.get ctxt trace then warning ("Blast: " ^ s) else (); Seq.empty);
@@ -1271,7 +1272,6 @@
     (Object_Logic.atomize_prems_tac 1 THEN
       raw_blast (Timing.start ()) ctxt lim) i st;
 
-
 fun blast_tac ctxt i st =
   let
     val start = Timing.start ();
@@ -1279,8 +1279,7 @@
   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
+      DEEPEN (1, lim) (fn m => fn _ => raw_blast start ctxt m) 0 1) i st
   end;