1.1 --- a/src/HOL/TPTP/mash_export.ML	Fri Jul 20 22:19:45 2012 +0200
     1.2 +++ b/src/HOL/TPTP/mash_export.ML	Fri Jul 20 22:19:45 2012 +0200
     1.3 @@ -25,8 +25,8 @@
     1.4  struct
     1.5  
     1.6  open Sledgehammer_Fact
     1.7 -open Sledgehammer_Filter_Iter
     1.8 -open Sledgehammer_Filter_MaSh
     1.9 +open Sledgehammer_MePo
    1.10 +open Sledgehammer_MaSh
    1.11  
    1.12  fun thy_map_from_facts ths =
    1.13    ths |> sort (thm_ord o swap o pairself snd)
    1.14 @@ -204,8 +204,8 @@
    1.15              let
    1.16                val suggs =
    1.17                  old_facts
    1.18 -                |> Sledgehammer_Filter_Iter.iterative_relevant_facts ctxt params
    1.19 -                                prover max_relevant NONE hyp_ts concl_t
    1.20 +                |> Sledgehammer_MePo.iterative_relevant_facts ctxt params prover
    1.21 +                       max_relevant NONE hyp_ts concl_t
    1.22                  |> map (fn ((name, _), _) => name ())
    1.23                  |> sort string_ord
    1.24                val s = escape_meta name ^ ": " ^ escape_metas suggs ^ "\n"