# HG changeset patch
# User blanchet
# Date 1403793690 -7200
# Node ID 6c6a0ac70eac8b56c09089afd8042b240b80258c
# Parent  98fb25b9e578b1387b83c371a8b13079561af64a
incremental learning when learing several facts

diff -r 98fb25b9e578 -r 6c6a0ac70eac 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:30 2014 +0200
@@ -1530,7 +1530,8 @@
             isar_dependencies_of name_tabs th
 
         fun do_commit [] [] [] state = state
-          | do_commit learns relearns flops {access_G, xtabs, ffds, freqs, dirty_facts} =
+          | do_commit learns relearns flops
+              {access_G, xtabs as ((num_facts0, _), _), ffds, freqs, dirty_facts} =
             let
               val was_empty = Graph.is_empty access_G
 
@@ -1545,7 +1546,13 @@
                   (false, SOME names) => SOME (map #1 learns @ map #1 relearns @ names)
                 | _ => NONE)
 
-              val (ffds', freqs') = recompute_ffds_freqs_from_access_G access_G xtabs
+              val (ffds', freqs') =
+                if null relearns then
+                  recompute_ffds_freqs_from_learns
+                    (map (fn (name, _, feats, deps) => (name, feats, deps)) learns) xtabs num_facts0
+                    ffds freqs
+                else
+                  recompute_ffds_freqs_from_access_G access_G xtabs
             in
               if engine = MaSh_Py then
                 (MaSh_Py.learn ctxt overlord (save andalso null relearns) learns;