--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Wed Jun 18 14:19:42 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Wed Jun 18 15:23:40 2014 +0200
@@ -375,8 +375,7 @@
val params =
get_params Minimize thy (("provers", [default_minimize_prover]) :: override_params)
val goal = prop_of (#goal (Proof.goal state))
- val facts = nearly_all_facts ctxt false fact_override Symtab.empty
- Termtab.empty [] [] goal
+ val facts = nearly_all_facts ctxt false fact_override Symtab.empty Termtab.empty [] [] goal
val learn = mash_learn_proof ctxt params goal facts
in run_minimize params learn i (#add fact_override) state end
else if subcommand = messagesN then
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Wed Jun 18 14:19:42 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Wed Jun 18 15:23:40 2014 +0200
@@ -1619,9 +1619,9 @@
fun mash_can_suggest_facts ctxt overlord =
not (Graph.is_empty (#access_G (peek_state ctxt overlord I)))
-(* Generate more suggestions than requested, because some might be thrown out
- later for various reasons. *)
-fun generous_max_suggestions max_facts = 11 * max_facts div 10 + 20
+(* Generate more suggestions than requested, because some might be thrown out later for various
+ reasons (e.g., duplicates). *)
+fun generous_max_suggestions max_facts = 3 * max_facts div 2 + 25
val mepo_weight = 0.5
val mash_weight = 0.5