# HG changeset patch
# User bulwahn
# Date 1291629164 -3600
# Node ID ce78ef6a909b3f51d10bf5d07af4d6077fc07d11
# Parent  6604115019bf1f3bfa8e379580dd5a352924a523
adding timeout to try invocation in mutabelle

diff -r 6604115019bf -r ce78ef6a909b src/HOL/Mutabelle/mutabelle_extra.ML
--- a/src/HOL/Mutabelle/mutabelle_extra.ML	Mon Dec 06 10:52:43 2010 +0100
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Mon Dec 06 10:52:44 2010 +0100
@@ -148,7 +148,7 @@
   let
     val state = Proof.theorem NONE (K I) (map (single o rpair []) [t]) (ProofContext.init_global thy)
   in
-    case Try.invoke_try NONE state of
+    case Try.invoke_try (SOME (seconds 5.0)) state of
       true => (Solved, ([], NONE))
     | false => (Unsolved, ([], NONE))
   end