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

--- 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