clarified blast after change of SELECT_GOAL in 210bca64b894: do not smash flex-flex pairs of overall goal state (in analogy to maxidx) -- NB: Isar goal structure serves as natural boundary, e.g. in "by blast";

--- a/src/Provers/blast.ML	Wed Jan 01 14:32:31 2014 +0100
+++ b/src/Provers/blast.ML	Wed Jan 01 20:14:47 2014 +0100
@@ -1258,7 +1258,6 @@
           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);