# HG changeset patch
# User blanchet
# Date 1401458454 -7200
# Node ID afa80e25a5f3c58856a9c8b96a154e470f93f169
# Parent  4ddf5a8f8f3861afbb1e913bddcb86f523a03456
made 'Kuehlwein-style' be really like Python code, we now think

diff -r 4ddf5a8f8f38 -r afa80e25a5f3 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri May 30 15:15:41 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri May 30 16:00:54 2014 +0200
@@ -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))