# HG changeset patch
# User blanchet
# Date 1400756873 -7200
# Node ID 7a1167331c8cf482ceaec1c6e24cc5f8f052b533
# Parent  fcd25f2e3da6a588802ff06fb44ffcec75239f2f
disable weights that cause more harm than they help in kNN

diff -r fcd25f2e3da6 -r 7a1167331c8c src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu May 22 13:07:52 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu May 22 13:07:53 2014 +0200
@@ -1200,7 +1200,10 @@
     val facts = facts |> sort (crude_thm_ord o pairself snd o swap)
     val chained = facts |> filter (fn ((_, (scope, _)), _) => scope = Chained)
     val num_facts = length facts
-    val const_tab = fold (add_const_counts o prop_of o snd) facts Symtab.empty
+
+    (* Weights are currently ignored by SML naive Bayes and appear to hurt kNN more than they
+       help. *)
+    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)