# HG changeset patch
# User boehmes
# Date 1344328084 -7200
# Node ID e1752ccccc34921ea87b09749608ad0dd3ee127d
# Parent  3b414244acb152bd99ba57122aebcf4fcab37c61
increase defensive timeout that should typically not kick in thanks to solid time limits in Sledgehammer (otherwise, Mirabelle-based evaluations might be distorted)

diff -r 3b414244acb1 -r e1752ccccc34 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Mon Aug 06 22:12:17 2012 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Tue Aug 07 10:28:04 2012 +0200
@@ -533,7 +533,7 @@
     val max_new_mono_instancesLST =
       available_parameter args max_new_mono_instancesK max_new_mono_instancesK
     val max_mono_itersLST = available_parameter args max_mono_itersK max_mono_itersK
-    val hard_timeout = SOME (2 * timeout)
+    val hard_timeout = SOME (4 * timeout)
     val (msg, result) =
       run_sh prover_name prover type_enc strict max_facts slice lam_trans
         uncurried_aliases e_selection_heuristic term_order force_sos