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)