# HG changeset patch
# User blanchet
# Date 1403793690 -7200
# Node ID 98fb25b9e578b1387b83c371a8b13079561af64a
# Parent  a212bee30bba1a9e6710902bf244225af52f662c
tuning

diff -r a212bee30bba -r 98fb25b9e578 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
@@ -1410,8 +1410,7 @@
     |> pairself (map fact_of_raw_fact)
   end
 
-fun learn_wrt_access_graph ctxt (name, parents, feats, deps)
-    (learns, (access_G, (fact_xtab, feat_xtab))) =
+fun learn_wrt_access_graph ctxt (name, parents, feats, deps) (access_G, (fact_xtab, feat_xtab)) =
   let
     fun maybe_learn_from from (accum as (parents, access_G)) =
       try_graph ctxt "updating graph" accum (fn () =>
@@ -1424,10 +1423,10 @@
     val fact_xtab = maybe_add_to_xtab name fact_xtab
     val feat_xtab = fold maybe_add_to_xtab feats feat_xtab
   in
-    ((name, parents, feats, deps) :: learns, (access_G, (fact_xtab, feat_xtab)))
+    ((name, parents, feats, deps), (access_G, (fact_xtab, feat_xtab)))
   end
 
-fun relearn_wrt_access_graph ctxt (name, deps) (relearns, access_G) =
+fun relearn_wrt_access_graph ctxt (name, deps) access_G =
   let
     fun maybe_relearn_from from (accum as (parents, access_G)) =
       try_graph ctxt "updating graph" accum (fn () =>
@@ -1436,7 +1435,7 @@
       access_G |> Graph.map_node name (fn (_, feats, _) => (Automatic_Proof, feats, deps))
     val (deps, _) = ([], access_G) |> fold maybe_relearn_from deps
   in
-    ((name, deps) :: relearns, access_G)
+    ((name, deps), access_G)
   end
 
 fun flop_wrt_access_graph name =
@@ -1535,11 +1534,10 @@
             let
               val was_empty = Graph.is_empty access_G
 
-              (* TODO: use "fold_map" *)
               val (learns, (access_G, xtabs)) =
-                fold (learn_wrt_access_graph ctxt) learns ([], (access_G, xtabs))
+                fold_map (learn_wrt_access_graph ctxt) learns (access_G, xtabs)
               val (relearns, access_G) =
-                fold (relearn_wrt_access_graph ctxt) relearns ([], access_G)
+                fold_map (relearn_wrt_access_graph ctxt) relearns access_G
 
               val access_G = access_G |> fold flop_wrt_access_graph flops
               val dirty_facts =
@@ -1550,7 +1548,7 @@
               val (ffds', freqs') = recompute_ffds_freqs_from_access_G access_G xtabs
             in
               if engine = MaSh_Py then
-                (MaSh_Py.learn ctxt overlord (save andalso null relearns) (rev learns);
+                (MaSh_Py.learn ctxt overlord (save andalso null relearns) learns;
                  MaSh_Py.relearn ctxt overlord save relearns)
               else
                 ();