# HG changeset patch
# User paulson
# Date 1306754117 -3600
# Node ID c46107e6714bf7a88e44d2a87b08f870767143ad
# Parent  665623e695ea1821dfecf5be8e341da95b0252b5
Fix to exception THM 1 raised (line 212 of conv.ML), reported by Andreas Lochbihler

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;