# HG changeset patch
# User blanchet
# Date 1406757176 -7200
# Node ID 249f13fed1a6328c87763347b084f657507a31e6
# Parent  892e8e7a42b31f70ea00444a65ed9d4cb42125db
reduced preplay timeout to 1 s

diff -r 892e8e7a42b3 -r 249f13fed1a6 src/Doc/Sledgehammer/document/root.tex
--- a/src/Doc/Sledgehammer/document/root.tex	Wed Jul 30 23:52:56 2014 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex	Wed Jul 30 23:52:56 2014 +0200
@@ -519,7 +519,7 @@
 generated by Sledgehammer instead of \textit{metis} if the proof obviously
 requires type information or if \textit{metis} failed when Sledgehammer
 preplayed the proof. (By default, Sledgehammer tries to run \textit{metis} with
-various sets of option for up to 2~seconds each time to ensure that the generated
+various sets of option for up to 1~second each time to ensure that the generated
 one-line proofs actually work and to display timing information. This can be
 configured using the \textit{preplay\_timeout} and \textit{dont\_preplay}
 options (\S\ref{timeouts}).)
@@ -1373,7 +1373,7 @@
 Specifies the maximum number of seconds that the automatic provers should spend
 searching for a proof. This excludes problem preparation and is a soft limit.
 
-\opdefault{preplay\_timeout}{float}{\upshape 2}
+\opdefault{preplay\_timeout}{float}{\upshape 1}
 Specifies the maximum number of seconds that \textit{metis} or other proof
 methods should spend trying to ``preplay'' the found proof. If this option
 is set to 0, no preplaying takes place, and no timing information is displayed
diff -r 892e8e7a42b3 -r 249f13fed1a6 src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Wed Jul 30 23:52:56 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Wed Jul 30 23:52:56 2014 +0200
@@ -97,7 +97,7 @@
    ("smt_proofs", "smart"),
    ("slice", "true"),
    ("minimize", "smart"),
-   ("preplay_timeout", "2")]
+   ("preplay_timeout", "1")]
 
 val alias_params =
   [("prover", ("provers", [])), (* undocumented *)