1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Sat Jan 19 12:53:13 2013 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Sat Jan 19 17:42:12 2013 +0100
     1.3 @@ -65,6 +65,7 @@
     1.4      Proof.context -> params -> string -> int -> fact list
     1.5      -> string Symtab.table * string Symtab.table -> thm
     1.6      -> bool * string list
     1.7 +  val weight_mepo_facts : 'a list -> ('a * real) list
     1.8    val weight_mash_facts : 'a list -> ('a * real) list
     1.9    val find_mash_suggestions :
    1.10      int -> string list -> ('b * thm) list -> ('b * thm) list -> ('b * thm) list
    1.11 @@ -759,6 +760,13 @@
    1.12  fun is_fact_in_graph access_G get_th fact =
    1.13    can (Graph.get_node access_G) (nickname_of_thm (get_th fact))
    1.14  
    1.15 +(* FUDGE *)
    1.16 +fun weight_of_mepo_fact rank =
    1.17 +  Math.pow (0.62, log2 (Real.fromInt (rank + 1)))
    1.18 +
    1.19 +fun weight_mepo_facts facts =
    1.20 +  facts ~~ map weight_of_mepo_fact (0 upto length facts - 1)
    1.21 +
    1.22  val weight_raw_mash_facts = weight_mepo_facts
    1.23  val weight_mash_facts = weight_raw_mash_facts
    1.24  

     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML	Sat Jan 19 12:53:13 2013 +0100
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML	Sat Jan 19 17:42:12 2013 +0100
     2.3 @@ -18,7 +18,6 @@
     2.4    val const_names_in_fact :
     2.5      theory -> (string * typ -> term list -> bool * term list) -> term
     2.6      -> string list
     2.7 -  val weight_mepo_facts : 'a list -> ('a * real) list
     2.8    val mepo_suggested_facts :
     2.9      Proof.context -> params -> string -> int -> relevance_fudge option
    2.10      -> term list -> term -> fact list -> fact list
    2.11 @@ -510,13 +509,6 @@
    2.12                        "Total relevant: " ^ string_of_int (length accepts)))
    2.13    end
    2.14  
    2.15 -(* FUDGE *)
    2.16 -fun weight_of_mepo_fact rank =
    2.17 -  Math.pow (0.62, log2 (Real.fromInt (rank + 1)))
    2.18 -
    2.19 -fun weight_mepo_facts facts =
    2.20 -  facts ~~ map weight_of_mepo_fact (0 upto length facts - 1)
    2.21 -
    2.22  fun mepo_suggested_facts ctxt
    2.23          ({fact_thresholds = (thres0, thres1), ...} : params) prover
    2.24          max_facts fudge hyp_ts concl_t facts =