# HG changeset patch
# User blanchet
# Date 1403097820 -7200
# Node ID 0acfdb151e52820a3867b41a3a96835e44ff2d15
# Parent  01b68f625550798e3ad4bec86fd502ae78029958
more generous formula -- there are lots of duplicates out there

diff -r 01b68f625550 -r 0acfdb151e52 src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML
--- 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
diff -r 01b68f625550 -r 0acfdb151e52 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- 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