# HG changeset patch
# User blanchet
# Date 1358613732 -3600
# Node ID 23bb011a5832fa56f938e3755317de9befcb74c2
# Parent  7c07ade3c8e0bbf89613edd3b022a759aa3ad76e
tuning

diff -r 7c07ade3c8e0 -r 23bb011a5832 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Sat Jan 19 12:53:13 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Sat Jan 19 17:42:12 2013 +0100
@@ -65,6 +65,7 @@
     Proof.context -> params -> string -> int -> fact list
     -> string Symtab.table * string Symtab.table -> thm
     -> bool * string list
+  val weight_mepo_facts : 'a list -> ('a * real) list
   val weight_mash_facts : 'a list -> ('a * real) list
   val find_mash_suggestions :
     int -> string list -> ('b * thm) list -> ('b * thm) list -> ('b * thm) list
@@ -759,6 +760,13 @@
 fun is_fact_in_graph access_G get_th fact =
   can (Graph.get_node access_G) (nickname_of_thm (get_th fact))
 
+(* FUDGE *)
+fun weight_of_mepo_fact rank =
+  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)
+
 val weight_raw_mash_facts = weight_mepo_facts
 val weight_mash_facts = weight_raw_mash_facts
 
diff -r 7c07ade3c8e0 -r 23bb011a5832 src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML	Sat Jan 19 12:53:13 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML	Sat Jan 19 17:42:12 2013 +0100
@@ -18,7 +18,6 @@
   val const_names_in_fact :
     theory -> (string * typ -> term list -> bool * term list) -> term
     -> string 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
@@ -510,13 +509,6 @@
                       "Total relevant: " ^ string_of_int (length accepts)))
   end
 
-(* FUDGE *)
-fun weight_of_mepo_fact rank =
-  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)
-
 fun mepo_suggested_facts ctxt
         ({fact_thresholds = (thres0, thres1), ...} : params) prover
         max_facts fudge hyp_ts concl_t facts =