# HG changeset patch
# User blanchet
# Date 1391551878 -3600
# Node ID e04b75bd18e0216941bbe2d59fbf4b0066fce6bd
# Parent  253a029335a249739b7cd6747e7f3369164f788f
tuned slack

diff -r 253a029335a2 -r e04b75bd18e0 src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML	Tue Feb 04 23:11:18 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML	Tue Feb 04 23:11:18 2014 +0100
@@ -32,7 +32,7 @@
       comment)
   | keep_fastest_method_of_isar_step _ step = step
 
-val slack = seconds 0.1
+val slack = seconds 0.025
 
 fun minimize_isar_step_dependencies ctxt preplay_data
       (step as Prove (qs, xs, l, t, subproofs, (lfs0, gfs0), meths as meth :: _, comment)) =