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:30 2014 +0200
     1.3 @@ -1530,7 +1530,8 @@
     1.4              isar_dependencies_of name_tabs th
     1.5  
     1.6          fun do_commit [] [] [] state = state
     1.7 -          | do_commit learns relearns flops {access_G, xtabs, ffds, freqs, dirty_facts} =
     1.8 +          | do_commit learns relearns flops
     1.9 +              {access_G, xtabs as ((num_facts0, _), _), ffds, freqs, dirty_facts} =
    1.10              let
    1.11                val was_empty = Graph.is_empty access_G
    1.12  
    1.13 @@ -1545,7 +1546,13 @@
    1.14                    (false, SOME names) => SOME (map #1 learns @ map #1 relearns @ names)
    1.15                  | _ => NONE)
    1.16  
    1.17 -              val (ffds', freqs') = recompute_ffds_freqs_from_access_G access_G xtabs
    1.18 +              val (ffds', freqs') =
    1.19 +                if null relearns then
    1.20 +                  recompute_ffds_freqs_from_learns
    1.21 +                    (map (fn (name, _, feats, deps) => (name, feats, deps)) learns) xtabs num_facts0
    1.22 +                    ffds freqs
    1.23 +                else
    1.24 +                  recompute_ffds_freqs_from_access_G access_G xtabs
    1.25              in
    1.26                if engine = MaSh_Py then
    1.27                  (MaSh_Py.learn ctxt overlord (save andalso null relearns) learns;