# HG changeset patch
# User blanchet
# Date 1291843117 -3600
# Node ID dfbc8759415ff37601512384c8d1a84763dc6ac0
# Parent  1b796ffa83473fa18f03cb9617ad0b75897fbee3
lower fudge factor

diff -r 1b796ffa8347 -r dfbc8759415f src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed Dec 08 22:17:53 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed Dec 08 22:18:37 2010 +0100
@@ -154,7 +154,7 @@
    max_imperfect = 11.5,
    max_imperfect_exp = 1.0,
    threshold_divisor = 2.0,
-   ridiculous_threshold = 0.1}
+   ridiculous_threshold = 0.01}
 
 (* FUDGE (FIXME) *)
 val smt_relevance_fudge =