# HG changeset patch
# User blanchet
# Date 1343050350 -7200
# Node ID f30eb5eb7927e264338584f8d07d54fe998b9c92
# Parent  aaaec69db3dbb7443dcdea2e4f51edeaae231d72
include unknown local facts in MaSh

diff -r aaaec69db3db -r f30eb5eb7927 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Mon Jul 23 15:32:30 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Mon Jul 23 15:32:30 2012 +0200
@@ -59,7 +59,7 @@
   val mash_can_suggest_facts : Proof.context -> bool
   val mash_suggested_facts :
     Proof.context -> params -> string -> int -> term list -> term
-    -> ('a * thm) list -> (('a * thm) * real) list * ('a * thm) list
+    -> fact list -> (fact * real) list * fact list
   val mash_learn_proof :
     Proof.context -> params -> string -> term -> ('a * thm) list -> thm list
     -> unit
@@ -606,6 +606,10 @@
 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 mash_suggested_facts ctxt ({overlord, ...} : params) prover max_facts hyp_ts
                          concl_t facts =
   let
@@ -623,13 +627,15 @@
               (fact_G, mash_QUERY ctxt overlord (max_suggs_of max_facts)
                                   (parents, feats))
             end)
-    val selected =
+    val sels =
       facts |> suggested_facts suggs
             (* The weights currently returned by "mash.py" are too extreme to
                make any sense. *)
-            |> map fst |> weight_mepo_facts
-    val unknown = facts |> filter_out (is_fact_in_graph fact_G)
-  in (selected, unknown) end
+            |> 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
 
 fun add_to_fact_graph ctxt (name, parents, feats, deps) (adds, graph) =
   let