diff -r f6f455df1034 -r b45b1b217f43 src/Provers/blast.ML
--- 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);