# HG changeset patch
# User blanchet
# Date 1284623972 -7200
# Node ID 8893562a954bcb16d4a4dd468d2e067f248b47ce
# Parent  7e9879fbb7c56a3d6c4955e20e081b68fa5fadfc
prevent exception when calling "Mirabelle.can_apply" on empty proof sequence;
the Judgement Day logs sometimes had entries of the form
    at 970:26 (apply):
    ------------------
    ------------------
; these were apparently caused by this Mirabelle bug

diff -r 7e9879fbb7c5 -r 8893562a954b src/HOL/Mirabelle/Tools/mirabelle.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle.ML	Thu Sep 16 08:29:50 2010 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle.ML	Thu Sep 16 09:59:32 2010 +0200
@@ -159,9 +159,9 @@
     val {context = ctxt, facts, goal} = Proof.goal st
     val full_tac = HEADGOAL (Method.insert_tac facts THEN' tac ctxt)
   in
-    (case TimeLimit.timeLimit time (Seq.pull o full_tac) goal of
-      SOME _ => true
-    | NONE => false)
+    (case try (TimeLimit.timeLimit time (Seq.pull o full_tac)) goal of
+      SOME (SOME _) => true
+    | _ => false)
   end
 
 local