# HG changeset patch
# User blanchet
# Date 1403793703 -7200
# Node ID ba0fe0639bc8f76e83537591e9e9ebc5146b5235
# Parent  6c6a0ac70eac8b56c09089afd8042b240b80258c
right array indexing

diff -r 6c6a0ac70eac -r ba0fe0639bc8 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Jun 26 16:41:30 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Jun 26 16:41:43 2014 +0200
@@ -500,13 +500,10 @@
       end
 
     fun for i =
-      if i = num_facts then
-        ()
-      else
-        (learn_one (num_facts0 + i) (Vector.sub (featss, i)) (Vector.sub (depss, i));
-         for (i + 1))
+      if i = num_facts then ()
+      else (learn_one i (Vector.sub (featss, i)) (Vector.sub (depss, i)); for (i + 1))
   in
-    for 0;
+    for num_facts0;
     (Array.vector tfreq, Array.vector sfreq, Array.vector dffreq)
   end
 
@@ -657,8 +654,7 @@
   ((Graph.new_node (name, (kind, feats, deps)) access_G
     handle Graph.DUP _ => Graph.map_node name (K (kind, feats, deps)) access_G)
    |> fold (add_edge_to name) parents,
-  (maybe_add_to_xtab name fact_xtab,
-   fold maybe_add_to_xtab feats feat_xtab),
+  (add_to_xtab name fact_xtab, fold maybe_add_to_xtab feats feat_xtab),
   (name, feats, deps) :: learns)
 
 fun try_graph ctxt when def f =
@@ -1420,7 +1416,7 @@
     val (parents, access_G) = ([], access_G) |> fold maybe_learn_from parents
     val (deps, _) = ([], access_G) |> fold maybe_learn_from deps
 
-    val fact_xtab = maybe_add_to_xtab name fact_xtab
+    val fact_xtab = add_to_xtab name fact_xtab
     val feat_xtab = fold maybe_add_to_xtab feats feat_xtab
   in
     ((name, parents, feats, deps), (access_G, (fact_xtab, feat_xtab)))