# HG changeset patch
# User blanchet
# Date 1283335144 -7200
# Node ID 7c655a491bce51eaae52ec1d9e11c3eaef9f97a4
# Parent  504b9e1efd3302ad9f62b7fb6a9a7889d32a0e41
fiddled with fudge factor (based on Mirabelle)

diff -r 504b9e1efd33 -r 7c655a491bce src/HOL/Tools/Sledgehammer/metis_tactics.ML
--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Wed Sep 01 11:36:02 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Wed Sep 01 11:59:04 2010 +0200
@@ -814,7 +814,7 @@
    "by (metis X)", to prevent "Subgoal.FOCUS" from freezing the type variables.
    We don't do it for nonschematic facts "X" because this breaks a few proofs
    (in the rare and subtle case where a proof relied on extensionality not being
-   applied) and brings no benefits. *)
+   applied) and brings few benefits. *)
 val has_tvar =
   exists_type (exists_subtype (fn TVar _ => true | _ => false)) o prop_of
 fun method name mode =
diff -r 504b9e1efd33 -r 7c655a491bce src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Wed Sep 01 11:36:02 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Wed Sep 01 11:59:04 2010 +0200
@@ -332,7 +332,7 @@
 val elim_bonus = Unsynchronized.ref 0.15
 val simp_bonus = Unsynchronized.ref 0.15
 val local_bonus = Unsynchronized.ref 0.55
-val assum_bonus = Unsynchronized.ref 1.0
+val assum_bonus = Unsynchronized.ref 1.05
 val chained_bonus = Unsynchronized.ref 1.5
 
 fun locality_bonus General = 0.0