src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML
changeset 50383 4274b25ff4e7
parent 50382 cb564ff43c28
child 50608 5977de2993ac
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML	Wed Dec 05 13:25:06 2012 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML	Wed Dec 05 13:25:06 2012 +0100
     1.3 @@ -510,10 +510,12 @@
     1.4    end
     1.5  
     1.6  (* Ad hoc score function roughly based on Blanchette's Ringberg 2011 data. *)
     1.7 -fun weight_of_fact rank = Math.pow (1.5, 15.5 - 0.05 * Real.fromInt rank) + 15.0
     1.8 +(* FUDGE *)
     1.9 +fun weight_of_mepo_fact rank =
    1.10 +  Math.pow (1.5, 15.5 - 0.05 * Real.fromInt rank) + 15.0
    1.11  
    1.12  fun weight_mepo_facts facts =
    1.13 -  facts ~~ map weight_of_fact (0 upto length facts - 1)
    1.14 +  facts ~~ map weight_of_mepo_fact (0 upto length facts - 1)
    1.15  
    1.16  fun mepo_suggested_facts ctxt
    1.17          ({fact_thresholds = (thres0, thres1), ...} : params) prover