# HG changeset patch
# User blanchet
# Date 1292408789 -3600
# Node ID 4a7410be4dfccbb798fa550f0c04d6d1817fadf5
# Parent  d58157bb1ae7e2119eb380483943d7bac08ca6f0
crank up Metis's timeout for SMT solvers, since users love Metis

diff -r d58157bb1ae7 -r 4a7410be4dfc src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed Dec 15 11:26:29 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed Dec 15 11:26:29 2010 +0100
@@ -511,7 +511,7 @@
     | _ => false
   end
 
-val smt_metis_timeout = seconds 0.5
+val smt_metis_timeout = seconds 1.0
 
 fun can_apply_metis debug state i ths =
   can_apply smt_metis_timeout