# HG changeset patch
# User blanchet
# Date 1391370831 -3600
# Node ID 982e082cd2baca69cab5f9b5524839f2d908b8f8
# Parent  0ff946f0b764edbb35ae81b942009c2b733b6e4f
tuned factor

diff -r 0ff946f0b764 -r 982e082cd2ba src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML	Sun Feb 02 20:53:51 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML	Sun Feb 02 20:53:51 2014 +0100
@@ -93,10 +93,10 @@
   | try_merge _ _ = NONE
 
 val compress_degree = 2
-val merge_timeout_slack = 1.2
+val merge_timeout_slack = 1.25
 
 (* Precondition: The proof must be labeled canonically
-   (cf. "Slegehammer_Proof.relabel_proof_canonically"). *)
+   (cf. "Slegehammer_Isar_Proof.relabel_isar_proof_canonically"). *)
 fun compress_isar_proof compress_isar
     ({preplay_outcome, set_preplay_outcome, preplay_quietly, ...} : isar_preplay_data) proof =
   if compress_isar <= 1.0 then