1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Mon Aug 29 13:50:47 2011 -0700
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Tue Aug 30 14:12:55 2011 +0200
     1.3 @@ -160,9 +160,16 @@
     1.4      fun desc () =
     1.5        prover_description ctxt params name num_facts subgoal subgoal_count goal
     1.6      val problem =
     1.7 -      {state = state, goal = goal, subgoal = subgoal,
     1.8 -       subgoal_count = subgoal_count, facts = facts |> take num_facts,
     1.9 -       smt_filter = smt_filter}
    1.10 +      let
    1.11 +        val filter_induction =
    1.12 +          List.filter (fn fact =>
    1.13 +                         not (Sledgehammer_Provers.is_induction_fact fact))
    1.14 +      in {state = state, goal = goal, subgoal = subgoal,
    1.15 +         subgoal_count = subgoal_count, facts =
    1.16 +          ((ATP_Systems.is_ho_atp name |> not) ? filter_induction) facts
    1.17 +          |> take num_facts,
    1.18 +         smt_filter = smt_filter}
    1.19 +      end
    1.20      fun really_go () =
    1.21        problem
    1.22        |> get_minimizing_prover ctxt mode name params minimize_command
    1.23 @@ -260,9 +267,12 @@
    1.24        val {facts = chained_ths, goal, ...} = Proof.goal state
    1.25        val chained_ths = chained_ths |> normalize_chained_theorems
    1.26        val (_, hyp_ts, concl_t) = strip_subgoal ctxt goal i
    1.27 -      val facts = nearly_all_facts ctxt relevance_override chained_ths hyp_ts
    1.28 -                                   concl_t
    1.29 -      val _ = () |> not blocking ? kill_provers
    1.30 +      val targetting_ho_provers =
    1.31 +        List.foldr (fn (name, so_far) => (ATP_Systems.is_ho_atp name) orelse
    1.32 +                     so_far)
    1.33 +          false provers
    1.34 +      val facts = nearly_all_facts ctxt targetting_ho_provers relevance_override
    1.35 +                                   chained_ths hyp_ts concl_t      val _ = () |> not blocking ? kill_provers
    1.36        val _ = case find_first (not o is_prover_supported ctxt) provers of
    1.37                  SOME name => error ("No such prover: " ^ name ^ ".")
    1.38                | NONE => ()
    1.39 @@ -313,9 +323,9 @@
    1.40            |> (case is_appropriate_prop of
    1.41                  SOME is_app => filter (is_app o prop_of o snd)
    1.42                | NONE => I)
    1.43 -          |> relevant_facts ctxt relevance_thresholds max_max_relevant
    1.44 -                            is_built_in_const relevance_fudge relevance_override
    1.45 -                            chained_ths hyp_ts concl_t
    1.46 +          |> relevant_facts ctxt targetting_ho_provers relevance_thresholds
    1.47 +                            max_max_relevant is_built_in_const relevance_fudge
    1.48 +                            relevance_override chained_ths hyp_ts concl_t
    1.49            |> tap (fn facts =>
    1.50                       if debug then
    1.51                         label ^ plural_s (length provers) ^ ": " ^