merged

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri May 30 15:34:14 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri May 30 16:10:57 2014 +0200
@@ -460,7 +460,7 @@
     ret [] (Integer.max 0 (num_visible_facts - max_suggs))
   end
 
-val nb_def_prior_weight = 20 (* FUDGE *)
+val nb_def_prior_weight = 21 (* FUDGE *)
 
 (* TODO: Either use IDF or don't use it. See commented out code portions below. *)
 
@@ -497,7 +497,7 @@
 val nb_kuehlwein_style = false
 
 val nb_tau = if nb_kuehlwein_style then 0.05 else 0.02 (* FUDGE *)
-val nb_pos_weight = if nb_kuehlwein_style then 20.0 else 2.0 (* FUDGE *)
+val nb_pos_weight = if nb_kuehlwein_style then 10.0 else 2.0 (* FUDGE *)
 val nb_def_val = ~15.0 (* FUDGE *)
 
 fun naive_bayes_query _ (* num_facts *) num_visible_facts max_suggs feats (tfreq, sfreq (*, dffreq*)) =
@@ -523,7 +523,7 @@
 
         val fold_sfh =
           if nb_kuehlwein_style then
-            (fn (f, sf) => fn sow => sow - tfidf f * (tfreq / Math.ln (Real.fromInt sf)))
+            (fn (f, sf) => fn sow => sow - tfidf f * Math.ln (Real.fromInt sf / tfreq))
           else
             (fn (f, sf) => fn sow =>
                sow + tfidf f * Math.ln (1.0 + (1.0 - Real.fromInt sf) / tfreq))