--- 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
--- 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 =