src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML

 
 fun add_node kind name parents feats deps (access_G, (fact_xtab, feat_xtab), learns) =
   ((Graph.new_node (name, (kind, feats, deps)) access_G
     handle Graph.DUP _ => Graph.map_node name (K (kind, feats, deps)) access_G)
    |> fold (add_edge_to name) parents,
-  (add_to_xtab name fact_xtab, fold maybe_add_to_xtab feats feat_xtab),
+  (maybe_add_to_xtab name fact_xtab, fold maybe_add_to_xtab feats feat_xtab),
   (name, feats, deps) :: learns)
 
 fun try_graph ctxt when def f =
   f ()
   handle

 
     val access_G = access_G |> Graph.default_node (name, (Isar_Proof, feats, deps))
     val (parents, access_G) = ([], access_G) |> fold maybe_learn_from parents
     val (deps, _) = ([], access_G) |> fold maybe_learn_from deps
 
-    val fact_xtab = add_to_xtab name fact_xtab
+    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), (access_G, (fact_xtab, feat_xtab)))
   end
 

           | do_commit learns relearns flops
               {access_G, xtabs as ((num_facts0, _), _), ffds, freqs, dirty_facts} =
             let
               val was_empty = Graph.is_empty access_G
 
-              val (learns, (access_G, xtabs)) =
+              val (learns, (access_G', xtabs')) =
                 fold_map (learn_wrt_access_graph ctxt) learns (access_G, xtabs)
-              val (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 =
+              val (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' =
                 (case (was_empty, dirty_facts) of
                   (false, SOME names) => SOME (map #1 learns @ map #1 relearns @ names)
                 | _ => NONE)
 
               val (ffds', freqs') =
                 if null relearns then
                   recompute_ffds_freqs_from_learns
-                    (map (fn (name, _, feats, deps) => (name, feats, deps)) learns) xtabs num_facts0
+                    (map (fn (name, _, feats, deps) => (name, feats, deps)) learns) xtabs' num_facts0
                     ffds freqs
                 else
-                  recompute_ffds_freqs_from_access_G access_G xtabs
+                  recompute_ffds_freqs_from_access_G access_G''' xtabs'
             in
-              {access_G = access_G, xtabs = xtabs, ffds = ffds', freqs = freqs',
-               dirty_facts = dirty_facts}
+              {access_G = access_G''', xtabs = xtabs', ffds = ffds', freqs = freqs',
+               dirty_facts = dirty_facts'}
             end
 
         fun commit last learns relearns flops =
           (if debug andalso auto_level = 0 then Output.urgent_message "Committing..." else ();
            map_state ctxt (do_commit (rev learns) relearns flops);

            |> Par_List.map (apsnd (fn f => f ()))
       val mesh = mesh_facts (eq_snd (gen_eq_thm ctxt)) max_facts mess |> add_and_take
     in
       (case (fact_filter, mess) of
         (NONE, [(_, (mepo, _)), (_, (mash, _))]) =>
-        [(meshN, mesh), (mepoN, mepo |> map fst |> add_and_take),
+        [(meshN, mesh),
+         (mepoN, mepo |> map fst |> add_and_take),
          (mashN, mash |> map fst |> add_and_take)]
       | _ => [(effective_fact_filter, mesh)])
     end
 
 fun kill_learners () = Async_Manager.kill_threads MaShN "learner"