--- 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)