src/HOL/Mirabelle/Tools/mirabelle.ML
changeset 39451 8893562a954b
parent 39377 9e544eb396dc
child 39557 fe5722fce758
--- 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