reduced preplaying timeout, since (1) Isar proofs are getting better and better as alternatives; (2) the same timeout is used for each step in an Isar proof, where a lower timeout makes more sense

--- a/src/Doc/Sledgehammer/document/root.tex	Mon Feb 03 10:14:18 2014 +0100
+++ b/src/Doc/Sledgehammer/document/root.tex	Mon Feb 03 10:19:19 2014 +0100
@@ -528,7 +528,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 options for up to 3 seconds each time to ensure that the generated
+various sets of option for up to 2~seconds 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}).)
@@ -1350,7 +1350,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 3}
+\opdefault{preplay\_timeout}{float}{\upshape 2}
 Specifies the maximum number of seconds that \textit{metis} or \textit{smt}
 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 next to the

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Mon Feb 03 10:14:18 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Mon Feb 03 10:19:19 2014 +0100
@@ -98,7 +98,7 @@
    ("try0_isar", "true"),
    ("slice", "true"),
    ("minimize", "smart"),
-   ("preplay_timeout", "3")]
+   ("preplay_timeout", "2")]
 
 val alias_params =
   [("prover", ("provers", [])), (* undocumented *)