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 @@ -59,7 +59,7 @@
     1.4    val mash_can_suggest_facts : Proof.context -> bool
     1.5    val mash_suggested_facts :
     1.6      Proof.context -> params -> string -> int -> term list -> term
     1.7 -    -> ('a * thm) list -> (('a * thm) * real) list * ('a * thm) list
     1.8 +    -> fact list -> (fact * real) list * fact list
     1.9    val mash_learn_proof :
    1.10      Proof.context -> params -> string -> term -> ('a * thm) list -> thm list
    1.11      -> unit
    1.12 @@ -606,6 +606,10 @@
    1.13  fun is_fact_in_graph fact_G (_, th) =
    1.14    can (Graph.get_node fact_G) (nickname_of th)
    1.15  
    1.16 +fun interleave [] ys = ys
    1.17 +  | interleave xs [] = xs
    1.18 +  | interleave (x :: xs) (y :: ys) = x :: y :: interleave xs ys
    1.19 +
    1.20  fun mash_suggested_facts ctxt ({overlord, ...} : params) prover max_facts hyp_ts
    1.21                           concl_t facts =
    1.22    let
    1.23 @@ -623,13 +627,15 @@
    1.24                (fact_G, mash_QUERY ctxt overlord (max_suggs_of max_facts)
    1.25                                    (parents, feats))
    1.26              end)
    1.27 -    val selected =
    1.28 +    val sels =
    1.29        facts |> suggested_facts suggs
    1.30              (* The weights currently returned by "mash.py" are too extreme to
    1.31                 make any sense. *)
    1.32 -            |> map fst |> weight_mepo_facts
    1.33 -    val unknown = facts |> filter_out (is_fact_in_graph fact_G)
    1.34 -  in (selected, unknown) end
    1.35 +            |> map fst
    1.36 +    val (unk_global, unk_local) =
    1.37 +      facts |> filter_out (is_fact_in_graph fact_G)
    1.38 +            |> List.partition (fn ((_, (loc, _)), _) => loc = Global)
    1.39 +  in (interleave unk_local sels |> weight_mepo_facts, unk_global) end
    1.40  
    1.41  fun add_to_fact_graph ctxt (name, parents, feats, deps) (adds, graph) =
    1.42    let