make SML code closer to Python code when 'nb_kuehlwein_style' is true

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri May 30 15:15:02 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri May 30 15:15:41 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*)) =