1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Jul 24 18:46:38 2014 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Jul 24 18:46:38 2014 +0200
     1.3 @@ -555,7 +555,7 @@
     1.4    ((Graph.new_node (name, (kind, feats, deps)) access_G
     1.5      handle Graph.DUP _ => Graph.map_node name (K (kind, feats, deps)) access_G)
     1.6     |> fold (add_edge_to name) parents,
     1.7 -  (add_to_xtab name fact_xtab, fold maybe_add_to_xtab feats feat_xtab),
     1.8 +  (maybe_add_to_xtab name fact_xtab, fold maybe_add_to_xtab feats feat_xtab),
     1.9    (name, feats, deps) :: learns)
    1.10  
    1.11  fun try_graph ctxt when def f =
    1.12 @@ -1221,7 +1221,7 @@
    1.13      val (parents, access_G) = ([], access_G) |> fold maybe_learn_from parents
    1.14      val (deps, _) = ([], access_G) |> fold maybe_learn_from deps
    1.15  
    1.16 -    val fact_xtab = add_to_xtab name fact_xtab
    1.17 +    val fact_xtab = maybe_add_to_xtab name fact_xtab
    1.18      val feat_xtab = fold maybe_add_to_xtab feats feat_xtab
    1.19    in
    1.20      ((name, parents, feats, deps), (access_G, (fact_xtab, feat_xtab)))
    1.21 @@ -1331,13 +1331,13 @@
    1.22              let
    1.23                val was_empty = Graph.is_empty access_G
    1.24  
    1.25 -              val (learns, (access_G, xtabs)) =
    1.26 +              val (learns, (access_G', xtabs')) =
    1.27                  fold_map (learn_wrt_access_graph ctxt) learns (access_G, xtabs)
    1.28 -              val (relearns, access_G) =
    1.29 -                fold_map (relearn_wrt_access_graph ctxt) relearns access_G
    1.30 +              val (relearns, access_G'') =
    1.31 +                fold_map (relearn_wrt_access_graph ctxt) relearns access_G'
    1.32  
    1.33 -              val access_G = access_G |> fold flop_wrt_access_graph flops
    1.34 -              val dirty_facts =
    1.35 +              val access_G''' = access_G'' |> fold flop_wrt_access_graph flops
    1.36 +              val dirty_facts' =
    1.37                  (case (was_empty, dirty_facts) of
    1.38                    (false, SOME names) => SOME (map #1 learns @ map #1 relearns @ names)
    1.39                  | _ => NONE)
    1.40 @@ -1345,13 +1345,13 @@
    1.41                val (ffds', freqs') =
    1.42                  if null relearns then
    1.43                    recompute_ffds_freqs_from_learns
    1.44 -                    (map (fn (name, _, feats, deps) => (name, feats, deps)) learns) xtabs num_facts0
    1.45 +                    (map (fn (name, _, feats, deps) => (name, feats, deps)) learns) xtabs' num_facts0
    1.46                      ffds freqs
    1.47                  else
    1.48 -                  recompute_ffds_freqs_from_access_G access_G xtabs
    1.49 +                  recompute_ffds_freqs_from_access_G access_G''' xtabs'
    1.50              in
    1.51 -              {access_G = access_G, xtabs = xtabs, ffds = ffds', freqs = freqs',
    1.52 -               dirty_facts = dirty_facts}
    1.53 +              {access_G = access_G''', xtabs = xtabs', ffds = ffds', freqs = freqs',
    1.54 +               dirty_facts = dirty_facts'}
    1.55              end
    1.56  
    1.57          fun commit last learns relearns flops =
    1.58 @@ -1585,7 +1585,8 @@
    1.59      in
    1.60        (case (fact_filter, mess) of
    1.61          (NONE, [(_, (mepo, _)), (_, (mash, _))]) =>
    1.62 -        [(meshN, mesh), (mepoN, mepo |> map fst |> add_and_take),
    1.63 +        [(meshN, mesh),
    1.64 +         (mepoN, mepo |> map fst |> add_and_take),
    1.65           (mashN, mash |> map fst |> add_and_take)]
    1.66        | _ => [(effective_fact_filter, mesh)])
    1.67      end