# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1465570388 -3600
# Node ID d2d26ff708d7f9d2b58fbf35273687cc32cc5af0
# Parent  9a2377b96ffd6a707451dd01ffb4b974a87c770e
code to catch exception TERM in blast

diff -r 9a2377b96ffd -r d2d26ff708d7 src/Provers/blast.ML
--- a/src/Provers/blast.ML	Fri Jun 10 13:54:50 2016 +0100
+++ b/src/Provers/blast.ML	Fri Jun 10 15:53:08 2016 +0100
@@ -1266,7 +1266,9 @@
             | cell => (cond_tracing (trace orelse stats)
                         (fn () => Timing.message (Timing.result start) ^ " for reconstruction");
                        Seq.make(fn()=> cell))
-          end
+          end handle TERM _ =>
+            (cond_tracing trace (fn () => "PROOF RAISED EXN TERM for depth " ^ string_of_int lim);
+                       backtrack trace choices)
   in
     prove (state, start, [initBranch (mkGoal concl :: hyps, lim)], cont)
   end