# HG changeset patch
# User blanchet
# Date 1403889436 -7200
# Node ID c9e8cd8ec9e2bd1802e3068ebdc2b9d1caf9def8
# Parent  39b3562e9edca3bda2852fed855de697215a7d1e
correctly take weights into consideration

diff -r 39b3562e9edc -r c9e8cd8ec9e2 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Jun 27 18:27:37 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Jun 27 19:17:16 2014 +0200
@@ -241,14 +241,8 @@
 val encode_strs = map encode_str #> space_implode " "
 val decode_strs = space_explode " " #> filter_out (curry (op =) "") #> map decode_str
 
-(* Avoid scientific notation *)
-fun safe_str_of_real r =
-  if r < 0.00001 then "0.00001"
-  else if r >= 1000000.0 then "1000000"
-  else Markup.print_real r
-
 fun encode_feature (names, weight) =
-  encode_str names ^ (if Real.== (weight, 1.0) then "" else "=" ^ safe_str_of_real weight)
+  encode_str names ^ (if Real.== (weight, 1.0) then "" else "=" ^ Real.toString weight)
 
 val encode_features = map encode_feature #> space_implode " "
 
@@ -525,11 +519,12 @@
             SOME sf =>
             (res + fw0 * tfidf f * Math.ln (pos_weight * Real.fromInt sf / tfreq),
              Inttab.delete f sfh)
-          | NONE => (res + tfidf f * def_val, sfh))
+          | NONE => (res + fw0 * tfidf f * def_val, sfh))
 
         val (res, sfh) = fold fold_feats goal_feats (Math.ln tfreq, Vector.sub (sfreq, i))
 
-        fun fold_sfh (f, sf) sow = sow + tfidf f * Math.ln (1.0 + (1.0 - Real.fromInt sf) / tfreq)
+        fun fold_sfh (f, sf) sow =
+          sow + tfidf f * Math.ln (1.0 + (1.0 - Real.fromInt sf) / tfreq)
 
         val sum_of_weights = Inttab.fold fold_sfh sfh 0.0
       in