# HG changeset patch
# User blanchet
# Date 1305206959 -7200
# Node ID 7e4ac591d983e5daf228dc795dc0d6d211750089
# Parent  8005fc9b65ec5bea844925fc469c6238bd854d0c
reduced penalty associated with existential quantifiers

diff -r 8005fc9b65ec -r 7e4ac591d983 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu May 12 15:29:19 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu May 12 15:29:19 2011 +0200
@@ -169,7 +169,7 @@
    higher_order_irrel_weight = 1.05,
    abs_rel_weight = 0.5,
    abs_irrel_weight = 2.0,
-   skolem_irrel_weight = 0.75,
+   skolem_irrel_weight = 0.5,
    theory_const_rel_weight = 0.5,
    theory_const_irrel_weight = 0.25,
    chained_const_irrel_weight = 0.25,