1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Mon Jul 23 15:32:30 2012 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Mon Jul 23 15:32:30 2012 +0200
     1.3 @@ -624,9 +624,11 @@
     1.4  fun is_fact_in_graph fact_G (_, th) =
     1.5    can (Graph.get_node fact_G) (nickname_of th)
     1.6  
     1.7 -fun interleave [] ys = ys
     1.8 -  | interleave xs [] = xs
     1.9 -  | interleave (x :: xs) (y :: ys) = x :: y :: interleave xs ys
    1.10 +fun interleave 0 _ _ = []
    1.11 +  | interleave n [] ys = take n ys
    1.12 +  | interleave n xs [] = take n xs
    1.13 +  | interleave 1 (x :: _) _ = [x]
    1.14 +  | interleave n (x :: xs) (y :: ys) = x :: y :: interleave (n - 2) xs ys
    1.15  
    1.16  fun mash_suggested_facts ctxt ({overlord, ...} : params) prover max_facts hyp_ts
    1.17                           concl_t facts =
    1.18 @@ -652,8 +654,8 @@
    1.19              |> map fst
    1.20      val (unk_global, unk_local) =
    1.21        facts |> filter_out (is_fact_in_graph fact_G)
    1.22 -            |> List.partition (fn ((_, (loc, _)), _) => loc = Global)
    1.23 -  in (interleave unk_local sels |> weight_mepo_facts, unk_global) end
    1.24 +            |> List.partition (fn ((_, (scope, _)), _) => scope = Global)
    1.25 +  in (interleave max_facts unk_local sels |> weight_mepo_facts, unk_global) end
    1.26  
    1.27  fun add_to_fact_graph ctxt (name, parents, feats, deps) (adds, graph) =
    1.28    let
    1.29 @@ -672,7 +674,7 @@
    1.30      val hard_timeout = time_mult learn_timeout_slack timeout
    1.31      val birth_time = Time.now ()
    1.32      val death_time = Time.+ (birth_time, hard_timeout)
    1.33 -    val desc = ("machine learner for Sledgehammer", "")
    1.34 +    val desc = ("Machine learner for Sledgehammer", "")
    1.35    in Async_Manager.launch MaShN birth_time death_time desc task end
    1.36  
    1.37  fun freshish_name () =