# HG changeset patch
# User blanchet
# Date 1358464691 -3600
# Node ID 00d87ade2294e26b50f8e15f0b743e4104e4efff
# Parent  b85cb3049df9a67294ef5072e2d6f2ccefd9340b
optimization -- evaluate conversion to table only once

diff -r b85cb3049df9 -r 00d87ade2294 src/HOL/TPTP/mash_eval.ML
--- a/src/HOL/TPTP/mash_eval.ML	Thu Jan 17 23:53:55 2013 +0100
+++ b/src/HOL/TPTP/mash_eval.ML	Fri Jan 18 00:18:11 2013 +0100
@@ -111,8 +111,9 @@
           val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1
           val isar_deps = isar_dependencies_of name_tabs th
           val facts = facts |> filter (fn (_, th') => thm_ord (th', th) = LESS)
+          val find_suggs = find_suggested_facts facts
           fun get_facts [] compute = compute facts
-            | get_facts suggs _ = find_suggested_facts suggs facts
+            | get_facts suggs _ = find_suggs suggs
           val mepo_facts =
             get_facts mepo_suggs (fn _ =>
                 mepo_suggested_facts ctxt params prover slack_max_facts NONE
@@ -133,7 +134,7 @@
                            (mess_of mash_facts))
           val mesh_isar_facts = mesh_of mesh_isar_suggs mash_isar_facts
           val mesh_prover_facts = mesh_of mesh_prover_suggs mash_prover_facts
-          val isar_facts = find_suggested_facts isar_deps facts
+          val isar_facts = find_suggs isar_deps
           (* adapted from "mirabelle_sledgehammer.ML" *)
           fun set_file_name method (SOME dir) =
               let
diff -r b85cb3049df9 -r 00d87ade2294 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Jan 17 23:53:55 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Jan 18 00:18:11 2013 +0100
@@ -46,7 +46,7 @@
 
   val mash_unlearn : Proof.context -> unit
   val nickname_of_thm : thm -> string
-  val find_suggested_facts : string list -> ('b * thm) list -> ('b * thm) list
+  val find_suggested_facts : ('b * thm) list -> string list -> ('b * thm) list
   val mesh_facts :
     ('a * 'a -> bool) -> int -> (real * (('a * real) list * 'a list)) list
     -> 'a list
@@ -433,11 +433,11 @@
   else
     elided_backquote_thm 200 th
 
-fun find_suggested_facts suggs facts =
+fun find_suggested_facts facts =
   let
     fun add_fact (fact as (_, th)) = Symtab.default (nickname_of_thm th, fact)
     val tab = fold add_fact facts Symtab.empty
-  in map_filter (Symtab.lookup tab) suggs end
+  in map_filter (Symtab.lookup tab) end
 
 fun scaled_avg [] = 0
   | scaled_avg xs =
@@ -774,7 +774,7 @@
 fun find_mash_suggestions _ [] _ _ raw_unknown = ([], raw_unknown)
   | find_mash_suggestions max_facts suggs facts chained raw_unknown =
     let
-      val raw_mash = find_suggested_facts suggs facts
+      val raw_mash = find_suggested_facts facts suggs
       val unknown_chained =
         inter (Thm.eq_thm_prop o pairself snd) chained raw_unknown
       val proximity =