src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML

 
 fun add_to_xtab key (next, tab, keys) = (next + 1, Symtab.update_new (key, next) tab, key :: keys)
 
 fun map_array_at ary f i = Array.update (ary, i, f (Array.sub (ary, i)))
 
-fun query ctxt engine parents access_G max_suggs hints feats =
-  let
-    val visible_facts = Graph.all_preds access_G parents
+fun query ctxt engine visible_facts max_suggs (learns, hints, parents, feats) =
+  let
     val visible_fact_set = Symtab.make_set visible_facts
 
-    val all_nodes =
-      (Graph.schedule (fn _ => fn (fact, (_, feats, deps)) => (fact, feats, deps)) access_G
-       |> List.partition (Symtab.defined visible_fact_set o #1) |> op @) @
+    val learns' =
+      (learns |> List.partition (Symtab.defined visible_fact_set o #1) |> op @) @
       (if null hints then [] else [(".goal", feats, hints)])
 
     val (rev_depss, rev_featss, (num_facts, _, rev_facts), (num_feats, feat_tab, _)) =
       fold (fn (fact, feats, deps) =>
             fn (rev_depss, rev_featss, fact_xtab as (_, fact_tab, _), feat_xtab) =>

             val (feats', feat_xtab') = fold_map add_feat feats feat_xtab
           in
             (map_filter (Symtab.lookup fact_tab) deps :: rev_depss, feats' :: rev_featss,
              add_to_xtab fact fact_xtab, feat_xtab')
           end)
-        all_nodes ([], [], (0, Symtab.empty, []), (0, Symtab.empty, []))
+        learns' ([], [], (0, Symtab.empty, []), (0, Symtab.empty, []))
 
     val facts = rev rev_facts
     val fact_vec = Vector.fromList facts
 
     val deps_vec = Vector.fromList (rev rev_depss)

 
     val sml_suggs =
       if engine = MaSh_Py then
         []
       else
-        let val (parents, hints, feats) = query_args access_G in
-          MaSh_SML.query ctxt engine parents access_G max_facts hints feats
+        let
+          val (parents, hints, feats) = query_args access_G
+          val visible_facts = Graph.all_preds access_G parents
+          val learns =
+            Graph.schedule (fn _ => fn (fact, (_, feats, deps)) => (fact, feats, deps)) access_G
+        in
+          MaSh_SML.query ctxt engine visible_facts max_facts (learns, hints, parents, feats)
         end
 
     val unknown = filter_out (is_fact_in_graph access_G o snd) facts
   in
     find_mash_suggestions ctxt max_facts (py_suggs @ sml_suggs) facts chained unknown