1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Jun 26 13:35:30 2014 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Jun 26 13:35:36 2014 +0200
     1.3 @@ -629,7 +629,10 @@
     1.4    c_plus_plus_tool ("newknn/knn" ^ " " ^ string_of_int number_of_nearest_neighbors)
     1.5  val naive_bayes_cpp = c_plus_plus_tool "predict/nbayes"
     1.6  
     1.7 +val empty_xtab = (0, Symtab.empty)
     1.8 +
     1.9  fun add_to_xtab key (next, tab) = (next + 1, Symtab.update_new (key, next) tab)
    1.10 +fun maybe_add_to_xtab key = perhaps (try (add_to_xtab key))
    1.11  
    1.12  fun map_array_at ary f i = Array.update (ary, i, f (Array.sub (ary, i)))
    1.13  
    1.14 @@ -643,28 +646,18 @@
    1.15        naive_bayes_cpp max_suggs learns feats
    1.16      else
    1.17        let
    1.18 -        val (rev_depss, rev_featss, ((num_facts, fact_tab), rev_facts), (num_feats, feat_tab)) =
    1.19 -          fold (fn (fact, feats, deps) =>
    1.20 -                fn (rev_depss, rev_featss, (fact_xtab as (_, fact_tab), rev_facts), feat_xtab) =>
    1.21 -              let
    1.22 -                fun add_feat feat (xtab as (n, tab)) =
    1.23 -                  (case Symtab.lookup tab feat of
    1.24 -                    SOME i => (i, xtab)
    1.25 -                  | NONE => (n, add_to_xtab feat xtab))
    1.26 +        val facts = map #1 learns
    1.27 +        val fact_vec = Vector.fromList facts
    1.28  
    1.29 -                val (feats', feat_xtab') = fold_map add_feat feats feat_xtab
    1.30 -              in
    1.31 -                (map_filter (Symtab.lookup fact_tab) deps :: rev_depss, feats' :: rev_featss,
    1.32 -                 (add_to_xtab fact fact_xtab, fact :: rev_facts), feat_xtab')
    1.33 -              end)
    1.34 -            learns ([], [], ((0, Symtab.empty), []), (0, Symtab.empty))
    1.35 +        val fact_xtab as (num_facts, fact_tab) = fold add_to_xtab facts empty_xtab
    1.36 +        val feat_xtab as (num_feats, feat_tab) = fold (fold maybe_add_to_xtab o #2) learns empty_xtab
    1.37  
    1.38 -        val facts = rev rev_facts
    1.39 -        val fact_vec = Vector.fromList facts
    1.40 +        val featss = map (map_filter (Symtab.lookup feat_tab) o #2) learns
    1.41 +
    1.42 +        val deps_vec = Vector.fromList (map (map_filter (Symtab.lookup fact_tab) o #3) learns)
    1.43 +
    1.44          val int_visible_facts = map_filter (Symtab.lookup fact_tab) visible_facts
    1.45  
    1.46 -        val deps_vec = Vector.fromList (rev rev_depss)
    1.47 -
    1.48          val get_deps = curry Vector.sub deps_vec
    1.49  
    1.50          val int_feats = map_filter (Symtab.lookup feat_tab) feats
    1.51 @@ -676,10 +669,8 @@
    1.52               val facts_ary = Array.array (num_feats, [])
    1.53               val _ =
    1.54                 fold (fn feats => fn fact =>
    1.55 -                   let val fact' = fact - 1 in
    1.56 -                     List.app (map_array_at facts_ary (cons fact')) feats; fact'
    1.57 -                   end)
    1.58 -                 rev_featss num_facts
    1.59 +                   (List.app (map_array_at facts_ary (cons fact)) feats; fact + 1))
    1.60 +                 featss 0
    1.61               val get_facts = curry Array.sub facts_ary
    1.62             in
    1.63               k_nearest_neighbors num_facts get_deps get_facts max_suggs int_visible_facts num_feats
    1.64 @@ -687,7 +678,7 @@
    1.65             end
    1.66           else
    1.67             let
    1.68 -             val unweighted_feats_ary = Vector.fromList (rev rev_featss)
    1.69 +             val unweighted_feats_ary = Vector.fromList featss
    1.70               val get_unweighted_feats = curry Vector.sub unweighted_feats_ary
    1.71             in
    1.72               (case engine of