1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Jul 20 22:19:46 2012 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Jul 20 22:43:51 2012 +0200
     1.3 @@ -613,7 +613,11 @@
     1.4      val suggs =
     1.5        if Graph.is_empty fact_G then []
     1.6        else mash_QUERY ctxt overlord (max_suggs_of max_facts) (parents, feats)
     1.7 -    val selected = facts |> suggested_facts suggs
     1.8 +    val selected =
     1.9 +      facts |> suggested_facts suggs
    1.10 +            (* The weights currently returned by "mash.py" are too extreme to
    1.11 +               make any sense. *)
    1.12 +            |> map fst |> weight_mepo_facts
    1.13      val unknown = facts |> filter_out (is_fact_in_graph fact_G)
    1.14    in (selected, unknown) end
    1.15  
    1.16 @@ -653,7 +657,7 @@
    1.17            val feats = features_of ctxt prover thy (Local, General) [t]
    1.18            val deps = used_ths |> map nickname_of
    1.19            val {fact_G} = mash_get ctxt
    1.20 -          val parents = timeit (fn () => maximal_in_graph fact_G facts)
    1.21 +          val parents = maximal_in_graph fact_G facts
    1.22          in
    1.23            mash_ADD ctxt overlord [(name, parents, feats, deps)]; (true, "")
    1.24          end)

     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML	Fri Jul 20 22:19:46 2012 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML	Fri Jul 20 22:43:51 2012 +0200
     2.3 @@ -21,7 +21,7 @@
     2.4    val mepo_suggested_facts :
     2.5      Proof.context -> params -> string -> int -> relevance_fudge option
     2.6      -> term list -> term -> fact list -> fact list
     2.7 -  val weight_mepo_facts : fact list -> (fact * real) list
     2.8 +  val weight_mepo_facts : ('a * thm) list -> (('a * thm) * real) list
     2.9  end;
    2.10  
    2.11  structure Sledgehammer_MePo : SLEDGEHAMMER_MEPO =