1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Jun 26 16:41:30 2014 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Jun 26 16:41:43 2014 +0200
     1.3 @@ -500,13 +500,10 @@
     1.4        end
     1.5  
     1.6      fun for i =
     1.7 -      if i = num_facts then
     1.8 -        ()
     1.9 -      else
    1.10 -        (learn_one (num_facts0 + i) (Vector.sub (featss, i)) (Vector.sub (depss, i));
    1.11 -         for (i + 1))
    1.12 +      if i = num_facts then ()
    1.13 +      else (learn_one i (Vector.sub (featss, i)) (Vector.sub (depss, i)); for (i + 1))
    1.14    in
    1.15 -    for 0;
    1.16 +    for num_facts0;
    1.17      (Array.vector tfreq, Array.vector sfreq, Array.vector dffreq)
    1.18    end
    1.19  
    1.20 @@ -657,8 +654,7 @@
    1.21    ((Graph.new_node (name, (kind, feats, deps)) access_G
    1.22      handle Graph.DUP _ => Graph.map_node name (K (kind, feats, deps)) access_G)
    1.23     |> fold (add_edge_to name) parents,
    1.24 -  (maybe_add_to_xtab name fact_xtab,
    1.25 -   fold maybe_add_to_xtab feats feat_xtab),
    1.26 +  (add_to_xtab name fact_xtab, fold maybe_add_to_xtab feats feat_xtab),
    1.27    (name, feats, deps) :: learns)
    1.28  
    1.29  fun try_graph ctxt when def f =
    1.30 @@ -1420,7 +1416,7 @@
    1.31      val (parents, access_G) = ([], access_G) |> fold maybe_learn_from parents
    1.32      val (deps, _) = ([], access_G) |> fold maybe_learn_from deps
    1.33  
    1.34 -    val fact_xtab = maybe_add_to_xtab name fact_xtab
    1.35 +    val fact_xtab = add_to_xtab name fact_xtab
    1.36      val feat_xtab = fold maybe_add_to_xtab feats feat_xtab
    1.37    in
    1.38      ((name, parents, feats, deps), (access_G, (fact_xtab, feat_xtab)))