# HG changeset patch
# User blanchet
# Date 1403106144 -7200
# Node ID 31b35f5a5fdb845926fe6decdb799fe3503fe4d8
# Parent  49c51eeaa62341381330b2cd4593fd53ebcaf826
split parameter into two

diff -r 49c51eeaa623 -r 31b35f5a5fdb src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Wed Jun 18 14:31:32 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Wed Jun 18 17:42:24 2014 +0200
@@ -498,10 +498,11 @@
     for 0; (Array.vector tfreq, Array.vector sfreq (*, Array.vector dffreq *))
   end
 
-val nb_kuehlwein_style = false
+val nb_kuehlwein_style_log = false
+val nb_kuehlwein_style_params = false
 
-val nb_tau = if nb_kuehlwein_style then 0.05 else 0.02 (* FUDGE *)
-val nb_pos_weight = if nb_kuehlwein_style then 10.0 else 2.0 (* FUDGE *)
+val nb_tau = if nb_kuehlwein_style_params then 0.05 else 0.02 (* FUDGE *)
+val nb_pos_weight = if nb_kuehlwein_style_params 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*)) =
@@ -526,7 +527,7 @@
         val (res, sfh) = fold fold_feats feats (Math.ln tfreq, Vector.sub (sfreq, i))
 
         val fold_sfh =
-          if nb_kuehlwein_style then
+          if nb_kuehlwein_style_log then
             (fn (f, sf) => fn sow => sow - tfidf f * Math.ln (Real.fromInt sf / tfreq))
           else
             (fn (f, sf) => fn sow =>