1.1 --- a/src/HOL/TPTP/mash_eval.ML	Fri Jul 20 22:19:45 2012 +0200
     1.2 +++ b/src/HOL/TPTP/mash_eval.ML	Fri Jul 20 22:19:45 2012 +0200
     1.3 @@ -17,7 +17,7 @@
     1.4  struct
     1.5  
     1.6  open Sledgehammer_Fact
     1.7 -open Sledgehammer_Filter_MaSh
     1.8 +open Sledgehammer_MaSh
     1.9  
    1.10  val MePoN = "MePo"
    1.11  val MaShN = "MaSh"
    1.12 @@ -78,8 +78,8 @@
    1.13          val isar_deps = isabelle_dependencies_of all_names th
    1.14          val facts = facts |> filter (fn (_, th') => thm_ord (th', th) = LESS)
    1.15          val mepo_facts =
    1.16 -          Sledgehammer_Filter_Iter.iterative_relevant_facts ctxt params
    1.17 -              prover slack_max_facts NONE hyp_ts concl_t facts
    1.18 +          Sledgehammer_MePo.iterative_relevant_facts ctxt params prover
    1.19 +              slack_max_facts NONE hyp_ts concl_t facts
    1.20          val mash_facts = facts |> suggested_facts suggs
    1.21          val mess = [(mepo_facts, []), (mash_facts, [])]
    1.22          val mesh_facts = mesh_facts slack_max_facts mess