1.1 --- a/src/HOL/TPTP/mash_eval.ML	Thu Jan 17 23:53:55 2013 +0100
     1.2 +++ b/src/HOL/TPTP/mash_eval.ML	Fri Jan 18 00:18:11 2013 +0100
     1.3 @@ -111,8 +111,9 @@
     1.4            val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1
     1.5            val isar_deps = isar_dependencies_of name_tabs th
     1.6            val facts = facts |> filter (fn (_, th') => thm_ord (th', th) = LESS)
     1.7 +          val find_suggs = find_suggested_facts facts
     1.8            fun get_facts [] compute = compute facts
     1.9 -            | get_facts suggs _ = find_suggested_facts suggs facts
    1.10 +            | get_facts suggs _ = find_suggs suggs
    1.11            val mepo_facts =
    1.12              get_facts mepo_suggs (fn _ =>
    1.13                  mepo_suggested_facts ctxt params prover slack_max_facts NONE
    1.14 @@ -133,7 +134,7 @@
    1.15                             (mess_of mash_facts))
    1.16            val mesh_isar_facts = mesh_of mesh_isar_suggs mash_isar_facts
    1.17            val mesh_prover_facts = mesh_of mesh_prover_suggs mash_prover_facts
    1.18 -          val isar_facts = find_suggested_facts isar_deps facts
    1.19 +          val isar_facts = find_suggs isar_deps
    1.20            (* adapted from "mirabelle_sledgehammer.ML" *)
    1.21            fun set_file_name method (SOME dir) =
    1.22                let

     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Jan 17 23:53:55 2013 +0100
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Jan 18 00:18:11 2013 +0100
     2.3 @@ -46,7 +46,7 @@
     2.4  
     2.5    val mash_unlearn : Proof.context -> unit
     2.6    val nickname_of_thm : thm -> string
     2.7 -  val find_suggested_facts : string list -> ('b * thm) list -> ('b * thm) list
     2.8 +  val find_suggested_facts : ('b * thm) list -> string list -> ('b * thm) list
     2.9    val mesh_facts :
    2.10      ('a * 'a -> bool) -> int -> (real * (('a * real) list * 'a list)) list
    2.11      -> 'a list
    2.12 @@ -433,11 +433,11 @@
    2.13    else
    2.14      elided_backquote_thm 200 th
    2.15  
    2.16 -fun find_suggested_facts suggs facts =
    2.17 +fun find_suggested_facts facts =
    2.18    let
    2.19      fun add_fact (fact as (_, th)) = Symtab.default (nickname_of_thm th, fact)
    2.20      val tab = fold add_fact facts Symtab.empty
    2.21 -  in map_filter (Symtab.lookup tab) suggs end
    2.22 +  in map_filter (Symtab.lookup tab) end
    2.23  
    2.24  fun scaled_avg [] = 0
    2.25    | scaled_avg xs =
    2.26 @@ -774,7 +774,7 @@
    2.27  fun find_mash_suggestions _ [] _ _ raw_unknown = ([], raw_unknown)
    2.28    | find_mash_suggestions max_facts suggs facts chained raw_unknown =
    2.29      let
    2.30 -      val raw_mash = find_suggested_facts suggs facts
    2.31 +      val raw_mash = find_suggested_facts facts suggs
    2.32        val unknown_chained =
    2.33          inter (Thm.eq_thm_prop o pairself snd) chained raw_unknown
    2.34        val proximity =