# HG changeset patch
# User blanchet
# Date 1403882310 -7200
# Node ID 140e16bc2a400ed2c9c752e2cfe0e089fc641f92
# Parent  e844dcf57debf128b36bdf5851fcbfc0fa9e61ea
use right theory name for theorems in evaluation driver

diff -r e844dcf57deb -r 140e16bc2a40 src/HOL/TPTP/mash_export.ML
--- a/src/HOL/TPTP/mash_export.ML	Fri Jun 27 17:05:22 2014 +0200
+++ b/src/HOL/TPTP/mash_export.ML	Fri Jun 27 17:18:30 2014 +0200
@@ -162,7 +162,7 @@
     val (new_facts, old_facts) = facts |> List.partition (has_thys thys o snd)
     val name_tabs = build_name_tables nickname_of_thm facts
 
-    fun do_fact (j, ((name, (parents, ((_, stature), th))), prevs)) =
+    fun do_fact (j, (name, (parents, ((_, stature), th)))) =
       if in_range range j then
         let
           val _ = tracing ("Fact " ^ string_of_int j ^ ": " ^ name)
@@ -205,9 +205,7 @@
 
     val new_facts =
       new_facts |> attach_parents_to_facts old_facts |> map (`(nickname_of_thm o snd o snd))
-    val hd_prevs = map (nickname_of_thm o snd) (the_list (try List.last old_facts))
-    val prevss = hd_prevs :: map (single o fst) new_facts |> split_last |> fst
-    val lines = map do_fact (tag_list 1 (new_facts ~~ prevss))
+    val lines = map do_fact (tag_list 1 new_facts)
   in
     File.write_list path lines
   end
@@ -243,7 +241,8 @@
               val suggs =
                 old_facts
                 |> filter_accessible_from th
-                |> mepo_or_mash_suggested_facts ctxt params max_suggs hyp_ts concl_t
+                |> mepo_or_mash_suggested_facts ctxt (theory_of_thm th) params max_suggs hyp_ts
+                  concl_t
                 |> map (nickname_of_thm o snd)
             in
               encode_str name ^ ": " ^ encode_strs suggs ^ "\n"
@@ -261,18 +260,18 @@
 
 val generate_mepo_suggestions =
   generate_mepo_or_mash_suggestions
-    (fn ctxt => fn params => fn max_suggs => fn hyp_ts => fn concl_t =>
+    (fn ctxt => fn _ => fn params => fn max_suggs => fn hyp_ts => fn concl_t =>
        not (Config.get ctxt Sledgehammer_MaSh.duplicates) ? Sledgehammer_Fact.drop_duplicate_facts
        #> Sledgehammer_MePo.mepo_suggested_facts ctxt params max_suggs NONE hyp_ts concl_t)
 
 fun generate_mash_suggestions ctxt params =
   (Sledgehammer_MaSh.mash_unlearn ctxt params;
    generate_mepo_or_mash_suggestions
-     (fn ctxt => fn params as {provers = prover :: _, ...} => fn max_suggs => fn hyp_ts =>
+     (fn ctxt => fn thy => fn params as {provers = prover :: _, ...} => fn max_suggs => fn hyp_ts =>
           fn concl_t =>
         tap (Sledgehammer_MaSh.mash_learn_facts ctxt params prover true 2 false
           Sledgehammer_Util.one_year)
-        #> Sledgehammer_MaSh.mash_suggested_facts ctxt params max_suggs hyp_ts concl_t
+        #> Sledgehammer_MaSh.mash_suggested_facts ctxt thy params max_suggs hyp_ts concl_t
         #> fst) ctxt params)
 
 fun generate_mesh_suggestions max_suggs mash_file_name mepo_file_name mesh_file_name =
diff -r e844dcf57deb -r 140e16bc2a40 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Jun 27 17:05:22 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Jun 27 17:18:30 2014 +0200
@@ -67,8 +67,8 @@
   val weight_facts_steeply : 'a list -> ('a * real) list
   val find_mash_suggestions : Proof.context -> int -> string list -> ('b * thm) list ->
     ('b * thm) list -> ('b * thm) list -> ('b * thm) list * ('b * thm) list
-  val mash_suggested_facts : Proof.context -> params -> int -> term list -> term -> raw_fact list ->
-    fact list * fact list
+  val mash_suggested_facts : Proof.context -> theory -> params -> int -> term list -> term ->
+    raw_fact list -> fact list * fact list
   val mash_learn_proof : Proof.context -> params -> term -> ('a * thm) list -> thm list -> unit
   val mash_learn_facts : Proof.context -> params -> string -> bool -> int -> bool -> Time.time ->
     raw_fact list -> string
@@ -1289,9 +1289,8 @@
     (mesh_facts (eq_snd (gen_eq_thm ctxt)) max_facts mess, unknown)
   end
 
-fun mash_suggested_facts ctxt ({debug, overlord, ...} : params) max_suggs hyp_ts concl_t facts =
+fun mash_suggested_facts ctxt thy ({debug, overlord, ...} : params) max_suggs hyp_ts concl_t facts =
   let
-    val thy = Proof_Context.theory_of ctxt
     val thy_name = Context.theory_name thy
     val engine = the_mash_engine ()
 
@@ -1682,6 +1681,8 @@
     [("", [])]
   else
     let
+      val thy = Proof_Context.theory_of ctxt
+
       fun maybe_launch_thread min_num_facts_to_learn =
         if not (Async_Manager.has_running_threads MaShN) andalso
            Time.toSeconds timeout >= min_secs_for_learning then
@@ -1747,7 +1748,8 @@
          |> weight_facts_steeply, [])
 
       fun mash () =
-        mash_suggested_facts ctxt params (generous_max_suggestions max_facts) hyp_ts concl_t facts
+        mash_suggested_facts ctxt thy params (generous_max_suggestions max_facts) hyp_ts concl_t
+          facts
         |>> weight_facts_steeply
 
       val mess =