--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Mon Aug 29 13:50:47 2011 -0700
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Tue Aug 30 14:12:55 2011 +0200
@@ -160,9 +160,16 @@
fun desc () =
prover_description ctxt params name num_facts subgoal subgoal_count goal
val problem =
- {state = state, goal = goal, subgoal = subgoal,
- subgoal_count = subgoal_count, facts = facts |> take num_facts,
- smt_filter = smt_filter}
+ let
+ val filter_induction =
+ List.filter (fn fact =>
+ not (Sledgehammer_Provers.is_induction_fact fact))
+ in {state = state, goal = goal, subgoal = subgoal,
+ subgoal_count = subgoal_count, facts =
+ ((ATP_Systems.is_ho_atp name |> not) ? filter_induction) facts
+ |> take num_facts,
+ smt_filter = smt_filter}
+ end
fun really_go () =
problem
|> get_minimizing_prover ctxt mode name params minimize_command
@@ -260,9 +267,12 @@
val {facts = chained_ths, goal, ...} = Proof.goal state
val chained_ths = chained_ths |> normalize_chained_theorems
val (_, hyp_ts, concl_t) = strip_subgoal ctxt goal i
- val facts = nearly_all_facts ctxt relevance_override chained_ths hyp_ts
- concl_t
- val _ = () |> not blocking ? kill_provers
+ val targetting_ho_provers =
+ List.foldr (fn (name, so_far) => (ATP_Systems.is_ho_atp name) orelse
+ so_far)
+ false provers
+ val facts = nearly_all_facts ctxt targetting_ho_provers relevance_override
+ chained_ths hyp_ts concl_t val _ = () |> not blocking ? kill_provers
val _ = case find_first (not o is_prover_supported ctxt) provers of
SOME name => error ("No such prover: " ^ name ^ ".")
| NONE => ()
@@ -313,9 +323,9 @@
|> (case is_appropriate_prop of
SOME is_app => filter (is_app o prop_of o snd)
| NONE => I)
- |> relevant_facts ctxt relevance_thresholds max_max_relevant
- is_built_in_const relevance_fudge relevance_override
- chained_ths hyp_ts concl_t
+ |> relevant_facts ctxt targetting_ho_provers relevance_thresholds
+ max_max_relevant is_built_in_const relevance_fudge
+ relevance_override chained_ths hyp_ts concl_t
|> tap (fn facts =>
if debug then
label ^ plural_s (length provers) ^ ": " ^