# HG changeset patch
# User blanchet
# Date 1357322449 -3600
# Node ID 60203cb4dbb87e20b9521a549be213ca63530ae2
# Parent  30bcdd5c8e789e812ca2d23f44a5e0282d9b3570
tweaked fudge factor

diff -r 30bcdd5c8e78 -r 60203cb4dbb8 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Jan 04 13:03:21 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Jan 04 19:00:49 2013 +0100
@@ -1055,7 +1055,7 @@
 
 (* Generate more suggestions than requested, because some might be thrown out
    later for various reasons. *)
-fun generous_max_facts max_facts = max_facts + Int.min (50, max_facts)
+fun generous_max_facts max_facts = max_facts + Int.min (50, max_facts div 2)
 
 (* The threshold should be large enough so that MaSh doesn't kick in for Auto
    Sledgehammer and Try. *)