1.1 --- a/src/HOL/TPTP/mash_eval.ML	Fri Jul 20 22:19:46 2012 +0200
     1.2 +++ b/src/HOL/TPTP/mash_eval.ML	Fri Jul 20 22:19:46 2012 +0200
     1.3 @@ -78,26 +78,28 @@
     1.4          val isar_deps = isar_dependencies_of all_names th |> these
     1.5          val facts = facts |> filter (fn (_, th') => thm_ord (th', th) = LESS)
     1.6          val mepo_facts =
     1.7 -          Sledgehammer_MePo.iterative_relevant_facts ctxt params prover
     1.8 +          Sledgehammer_MePo.mepo_suggested_facts ctxt params prover
     1.9                slack_max_facts NONE hyp_ts concl_t facts
    1.10 -        val mash_facts = facts |> suggested_facts suggs
    1.11 +          |> Sledgehammer_MePo.weight_mepo_facts
    1.12 +        val mash_facts = suggested_facts suggs facts
    1.13          val mess = [(mepo_facts, []), (mash_facts, [])]
    1.14          val mesh_facts = mesh_facts slack_max_facts mess
    1.15 -        val isar_facts = suggested_facts isar_deps facts
    1.16 -        fun prove ok heading facts =
    1.17 +        val isar_facts = suggested_facts (map (rpair 1.0) isar_deps) facts
    1.18 +        fun prove ok heading get facts =
    1.19            let
    1.20              val facts =
    1.21 -              facts
    1.22 -              |> Sledgehammer_Fact.maybe_instantiate_inducts ctxt hyp_ts concl_t
    1.23 -              |> take (the max_facts)
    1.24 +              facts |> map get
    1.25 +                    |> Sledgehammer_Fact.maybe_instantiate_inducts ctxt hyp_ts
    1.26 +                                                                   concl_t
    1.27 +                    |> take (the max_facts)
    1.28              val res as {outcome, ...} =
    1.29                run_prover_for_mash ctxt params prover facts goal
    1.30              val _ = if is_none outcome then ok := !ok + 1 else ()
    1.31            in str_of_res heading facts res end
    1.32 -        val mepo_s = prove mepo_ok MePoN mepo_facts
    1.33 -        val mash_s = prove mash_ok MaShN mash_facts
    1.34 -        val mesh_s = prove mesh_ok MeshN mesh_facts
    1.35 -        val isar_s = prove isar_ok IsarN isar_facts
    1.36 +        val mepo_s = prove mepo_ok MePoN fst mepo_facts
    1.37 +        val mash_s = prove mash_ok MaShN fst mash_facts
    1.38 +        val mesh_s = prove mesh_ok MeshN I mesh_facts
    1.39 +        val isar_s = prove isar_ok IsarN fst isar_facts
    1.40        in
    1.41          ["Goal " ^ string_of_int j ^ ": " ^ name, mepo_s, mash_s, mesh_s,
    1.42           isar_s]