1.1 --- a/src/HOL/TPTP/mash_export.ML	Wed Jul 18 08:44:03 2012 +0200
     1.2 +++ b/src/HOL/TPTP/mash_export.ML	Wed Jul 18 08:44:03 2012 +0200
     1.3 @@ -46,7 +46,8 @@
     1.4      val parents = parent_thms thy_ths thy
     1.5    in fold do_fact new_facts parents; () end
     1.6  
     1.7 -fun generate_iter_suggestions ctxt params thy max_relevant file_name =
     1.8 +fun generate_iter_suggestions ctxt (params as {provers, ...}) thy max_relevant
     1.9 +                              file_name =
    1.10    let
    1.11      val path = file_name |> Path.explode
    1.12      val _ = File.write path ""
    1.13 @@ -58,14 +59,17 @@
    1.14        let
    1.15          val name = Thm.get_name_hint th
    1.16          val goal = goal_of_thm thy th
    1.17 +        val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1
    1.18          val kind = Thm.legacy_get_kind th
    1.19          val _ =
    1.20            if kind <> "" then
    1.21              let
    1.22                val suggs =
    1.23 -                old_facts |> iter_facts ctxt params max_relevant goal
    1.24 -                          |> map (fn ((name, _), _) => fact_name_of (name ()))
    1.25 -                          |> sort string_ord
    1.26 +                old_facts
    1.27 +                |> Sledgehammer_Filter_Iter.iterative_relevant_facts ctxt params
    1.28 +                                (hd provers) max_relevant NONE hyp_ts concl_t
    1.29 +                |> map (fn ((name, _), _) => fact_name_of (name ()))
    1.30 +                |> sort string_ord
    1.31                val s = fact_name_of name ^ ": " ^ space_implode " " suggs ^ "\n"
    1.32              in File.append path s end
    1.33            else