# HG changeset patch
# User blanchet
# Date 1403782490 -7200
# Node ID dd89d0ec8e41bd556685dbd536c046ed2f6645bd
# Parent  545d02691b328e36e57a4cae84edfec02c336b94
avoid subscripting array with ~1

diff -r 545d02691b32 -r dd89d0ec8e41 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Jun 26 13:34:39 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Jun 26 13:34:50 2014 +0200
@@ -438,7 +438,7 @@
     val _ = for1 0
 
     val ln_afreq = Math.ln (Real.fromInt num_facts)
-    fun tfidf feat = ln_afreq - Math.ln (Real.fromInt (Array.sub (dffreq, feat))) handle Subscript => ln_afreq
+    fun tfidf feat = ln_afreq - Math.ln (Real.fromInt (Array.sub (dffreq, feat)))
 
     val overlaps_sqr = Array.tabulate (num_facts, rpair 0.0)
 
@@ -550,8 +550,7 @@
     val pos_weight = if kuehlwein_params then 10.0 else 2.0 (* FUDGE *)
     val def_val = ~15.0 (* FUDGE *)
 
-    val ln_afreq = Math.ln (Real.fromInt num_facts)
-    fun tfidf feat = Vector.sub (idf, feat) handle Subscript => ln_afreq (* TODO: clean up *)
+    fun tfidf feat = Vector.sub (idf, feat)
 
     fun log_posterior i =
       let
@@ -687,7 +686,7 @@
 
         val get_deps = curry Vector.sub deps_vec
 
-        val int_feats = map (the_default ~1 o Symtab.lookup feat_tab) feats
+        val int_feats = map_filter (Symtab.lookup feat_tab) feats
       in
         trace_msg ctxt (fn () => "MaSh_SML query " ^ encode_strs feats ^ " from {" ^
           elide_string 1000 (space_implode " " (take num_facts facts)) ^ "}");