src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML

 fun max_suggs_of max_facts = max_facts + Int.min (50, max_facts)
 
 fun is_fact_in_graph fact_G (_, th) =
   can (Graph.get_node fact_G) (nickname_of th)
 
-fun interleave [] ys = ys
-  | interleave xs [] = xs
-  | interleave (x :: xs) (y :: ys) = x :: y :: interleave xs ys
+fun interleave 0 _ _ = []
+  | interleave n [] ys = take n ys
+  | interleave n xs [] = take n xs
+  | interleave 1 (x :: _) _ = [x]
+  | interleave n (x :: xs) (y :: ys) = x :: y :: interleave (n - 2) xs ys
 
 fun mash_suggested_facts ctxt ({overlord, ...} : params) prover max_facts hyp_ts
                          concl_t facts =
   let
     val thy = Proof_Context.theory_of ctxt

             (* The weights currently returned by "mash.py" are too extreme to
                make any sense. *)
             |> map fst
     val (unk_global, unk_local) =
       facts |> filter_out (is_fact_in_graph fact_G)
-            |> List.partition (fn ((_, (loc, _)), _) => loc = Global)
-  in (interleave unk_local sels |> weight_mepo_facts, unk_global) end
+            |> List.partition (fn ((_, (scope, _)), _) => scope = Global)
+  in (interleave max_facts unk_local sels |> weight_mepo_facts, unk_global) end
 
 fun add_to_fact_graph ctxt (name, parents, feats, deps) (adds, graph) =
   let
     fun maybe_add_from from (accum as (parents, graph)) =
       try_graph ctxt "updating graph" accum (fn () =>

 fun launch_thread timeout task =
   let
     val hard_timeout = time_mult learn_timeout_slack timeout
     val birth_time = Time.now ()
     val death_time = Time.+ (birth_time, hard_timeout)
-    val desc = ("machine learner for Sledgehammer", "")
+    val desc = ("Machine learner for Sledgehammer", "")
   in Async_Manager.launch MaShN birth_time death_time desc task end
 
 fun freshish_name () =
   Date.fmt ".%Y_%m_%d_%H_%M_%S__" (Date.fromTimeLocal (Time.now ())) ^
   serial_string ()