diff -r e928f8647302 -r 5977de2993ac src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML	Thu Dec 20 15:51:24 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML	Thu Dec 20 15:51:27 2012 +0100
@@ -18,7 +18,7 @@
   val const_names_in_fact :
     theory -> (string * typ -> term list -> bool * term list) -> term
     -> string list
-  val weight_mepo_facts : ('a * thm) list -> (('a * thm) * real) list
+  val weight_mepo_facts : 'a list -> ('a * real) list
   val mepo_suggested_facts :
     Proof.context -> params -> string -> int -> relevance_fudge option
     -> term list -> term -> fact list -> fact list
@@ -28,6 +28,7 @@
 struct
 
 open ATP_Problem_Generate
+open Sledgehammer_Util
 open Sledgehammer_Fact
 open Sledgehammer_Provers
 
@@ -509,10 +510,9 @@
                       "Total relevant: " ^ string_of_int (length accepts)))
   end
 
-(* Ad hoc score function roughly based on Blanchette's Ringberg 2011 data. *)
 (* FUDGE *)
 fun weight_of_mepo_fact rank =
-  Math.pow (1.5, 15.5 - 0.05 * Real.fromInt rank) + 15.0
+  Math.pow (0.62, log2 (Real.fromInt (rank + 1)))
 
 fun weight_mepo_facts facts =
   facts ~~ map weight_of_mepo_fact (0 upto length facts - 1)