--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Wed Aug 31 11:23:16 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Wed Aug 31 11:52:03 2011 +0200
@@ -269,9 +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 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 ho_atp = exists (Sledgehammer_Provers.is_ho_atp ctxt) provers
+ val facts =
+ nearly_all_facts ctxt 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 ^ ".")
@@ -323,9 +324,9 @@
|> (case is_appropriate_prop of
SOME is_app => filter (is_app o prop_of o snd)
| NONE => I)
- |> 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
+ |> relevant_facts ctxt 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) ^ ": " ^