# HG changeset patch
# User blanchet
# Date 1401264268 -7200
# Node ID 28618ccec4c77d526fe0237fc98310d1104fbd80
# Parent  f6fbed91fbd4a8df7db827bd3064b298b05eb494
enabled IDF for naive Bayes ML

diff -r f6fbed91fbd4 -r 28618ccec4c7 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Wed May 28 10:03:14 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Wed May 28 10:04:28 2014 +0200
@@ -454,8 +454,7 @@
         afreq := !afreq + 1
       end
 
-    fun tfidf _ = 1.0
-    (* fun tfidf sym = Math.ln (Real.fromInt (!afreq)) - Math.ln (Real.fromInt (Array.sub (dffreq, sym))) *)
+    fun tfidf sym = Math.ln (Real.fromInt (!afreq)) - Math.ln (Real.fromInt (Array.sub (dffreq, sym)))
 
     fun eval syms =
       let
@@ -1212,8 +1211,7 @@
     val num_facts = length facts
 
     (* Weights appear to hurt kNN more than they help. *)
-    val const_tab = Symtab.empty |> engine <> MaSh_SML_kNN
-      ? fold (add_const_counts o prop_of o snd) facts
+    val const_tab = Symtab.empty |> engine = MaSh_Py ? fold (add_const_counts o prop_of o snd) facts
 
     fun fact_has_right_theory (_, th) =
       thy_name = Context.theory_name (theory_of_thm th)