--- 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 =
--- 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