# HG changeset patch
# User blanchet
# Date 1401263054 -7200
# Node ID c0a25c7c4b8e65821dd538ead098889c3b05a346
# Parent  80b7c07e7a73e09b71d29e65ca76a068868dc535
repaired subscript problem in SML kNN

diff -r 80b7c07e7a73 -r c0a25c7c4b8e src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Wed May 28 09:38:39 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Wed May 28 09:44:14 2014 +0200
@@ -532,7 +532,6 @@
 
     val num_visible_facts = length visible_facts
     val get_deps = curry Vector.sub deps_vec
-    val syms = map (apfst (the_default ~1 o Symtab.lookup feat_tab)) feats
   in
     trace_msg ctxt (fn () => "MaSh_SML " ^ (if engine = MaSh_SML_kNN then "kNN" else "NB") ^
       " query " ^ encode_features feats ^ " from {" ^
@@ -549,6 +548,8 @@
                end)
              rev_featss num_facts
          val get_facts = curry Array.sub facts_ary
+         val syms = map_filter (fn (feat, weight) =>
+           Option.map (rpair weight) (Symtab.lookup feat_tab feat)) feats
        in
          k_nearest_neighbors num_facts num_visible_facts get_deps get_facts max_suggs syms
        end
@@ -556,6 +557,7 @@
        let
          val unweighted_feats_ary = Vector.fromList (map (map fst) (rev rev_featss))
          val get_unweighted_feats = curry Vector.sub unweighted_feats_ary
+         val syms = map (apfst (the_default ~1 o Symtab.lookup feat_tab)) feats
        in
          naive_bayes num_facts num_visible_facts get_deps get_unweighted_feats num_feats max_suggs
            syms