Merge

--- a/src/Provers/blast.ML	Fri Jun 10 16:36:24 2016 +0200
+++ b/src/Provers/blast.ML	Fri Jun 10 17:12:14 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