diff -r 665623e695ea -r c46107e6714b src/Provers/blast.ML
--- a/src/Provers/blast.ML	Fri May 27 10:41:09 2011 +0200
+++ b/src/Provers/blast.ML	Mon May 30 12:15:17 2011 +0100
@@ -1267,7 +1267,7 @@
     prove (state, start, [initBranch (mkGoal concl :: hyps, lim)], cont)
     |> Seq.map (rotate_prems (1 - i))
   end
-  handle PROVE => Seq.empty;
+  handle PROVE => Seq.empty | THM _ => Seq.empty;
 
 (*Public version with fixed depth*)
 fun depth_tac ctxt lim i st = timing_depth_tac (Timing.start ()) ctxt lim i st;