# HG changeset patch
# User blanchet
# Date 1401264194 -7200
# Node ID f6fbed91fbd4a8df7db827bd3064b298b05eb494
# Parent  c0a25c7c4b8e65821dd538ead098889c3b05a346
tuning

diff -r c0a25c7c4b8e -r f6fbed91fbd4 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Wed May 28 09:44:14 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Wed May 28 10:03:14 2014 +0200
@@ -455,7 +455,7 @@
       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
@@ -902,13 +902,14 @@
     fun add_subtypes (T as Type (_, Ts)) = add_type T #> fold add_subtypes Ts
       | add_subtypes T = add_type T
 
-    fun weight_of_const s =
-      16.0 +
-      (if num_facts = 0 then
-         0.0
+    val base_weight_of_const = 16.0 (* FUDGE *)
+    val weight_of_const =
+      (if num_facts = 0 orelse Symtab.is_empty const_tab then
+         K base_weight_of_const
        else
+         fn s =>
          let val count = Symtab.lookup const_tab s |> the_default 1 in
-           Real.fromInt num_facts / Real.fromInt count (* FUDGE *)
+           base_weight_of_const + Real.fromInt num_facts / Real.fromInt count
          end)
 
     fun pattify_term _ 0 _ = []