# HG changeset patch
# User blanchet
# Date 1328441230 -3600
# Node ID fd15abc50fc19ff957884d8c94c8f2e86e2c55c2
# Parent  0a37c1e52c917b7cd36e07069d525c56bc000233
tuning

diff -r 0a37c1e52c91 -r fd15abc50fc1 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Sun Feb 05 11:14:25 2012 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Sun Feb 05 12:27:10 2012 +0100
@@ -390,7 +390,6 @@
            ("strict", strict),
            ("lam_trans", lam_trans |> the_default "smart"),
            ("uncurried_aliases", uncurried_aliases |> the_default "smart"),
-           ("preplay_timeout", preplay_timeout),
            ("max_relevant", max_relevant),
            ("slice", slice),
            ("timeout", string_of_int timeout),