--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Tue Aug 30 14:12:55 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Tue Aug 30 14:12:55 2011 +0200
@@ -144,6 +144,9 @@
get_prover ctxt mode name params minimize_command problem
|> minimize ctxt mode name params problem
+fun is_induction_fact (Untranslated_Fact ((_, Induction), _)) = true
+ | is_induction_fact _ = false
+
fun launch_prover (params as {debug, verbose, blocking, max_relevant, slicing,
timeout, expect, ...})
mode minimize_command only
@@ -161,12 +164,11 @@
prover_description ctxt params name num_facts subgoal subgoal_count goal
val problem =
let
- val filter_induction =
- List.filter (fn fact =>
- not (Sledgehammer_Provers.is_induction_fact fact))
+ val filter_induction = filter_out is_induction_fact
in {state = state, goal = goal, subgoal = subgoal,
subgoal_count = subgoal_count, facts =
- ((ATP_Systems.is_ho_atp name |> not) ? filter_induction) facts
+ ((Sledgehammer_Provers.is_ho_atp ctxt name |> not) ? filter_induction)
+ facts
|> take num_facts,
smt_filter = smt_filter}
end
@@ -267,12 +269,10 @@
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 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 is_ho_atp = exists (Sledgehammer_Provers.is_ho_atp ctxt) provers
+ val facts = nearly_all_facts ctxt is_ho_atp 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 => ()
@@ -323,7 +323,7 @@
|> (case is_appropriate_prop of
SOME is_app => filter (is_app o prop_of o snd)
| NONE => I)
- |> relevant_facts ctxt targetting_ho_provers relevance_thresholds
+ |> relevant_facts ctxt is_ho_atp relevance_thresholds
max_max_relevant is_built_in_const relevance_fudge
relevance_override chained_ths hyp_ts concl_t
|> tap (fn facts =>