# HG changeset patch
# User blanchet
# Date 1337185011 -7200
# Node ID 08d7aff8c7e60c484bf7456d325301c8b3d7e697
# Parent  4e8e0245e8be9ca278e9076a4f08ff0007433861
lower skolem penalty to ensure that some useful facts with existentials, e.g. congruence of "setsum", eventually get picked up

diff -r 4e8e0245e8be -r 08d7aff8c7e6 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed May 16 18:16:51 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed May 16 18:16:51 2012 +0200
@@ -223,7 +223,7 @@
    higher_order_irrel_weight = 1.05,
    abs_rel_weight = 0.5,
    abs_irrel_weight = 2.0,
-   skolem_irrel_weight = 0.25,
+   skolem_irrel_weight = 0.05,
    theory_const_rel_weight = 0.5,
    theory_const_irrel_weight = 0.25,
    chained_const_irrel_weight = 0.25,