--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Tue May 24 00:01:33 2011 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Tue May 24 00:01:33 2011 +0200
@@ -118,8 +118,9 @@
val default_max_relevant =
Sledgehammer_Provers.default_max_relevant_for_prover ctxt slicing
prover
- val is_good_prop =
- Sledgehammer_Provers.is_good_prop_for_prover ctxt default_prover
+ val is_appropriate_prop =
+ Sledgehammer_Provers.is_appropriate_prop_for_prover ctxt
+ default_prover
val is_built_in_const =
Sledgehammer_Provers.is_built_in_const_for_prover ctxt default_prover
val relevance_fudge =
@@ -130,9 +131,9 @@
val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal subgoal
val facts =
Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds
- (the_default default_max_relevant max_relevant) is_good_prop
- is_built_in_const relevance_fudge relevance_override facts hyp_ts
- concl_t
+ (the_default default_max_relevant max_relevant)
+ is_appropriate_prop is_built_in_const relevance_fudge
+ relevance_override facts hyp_ts concl_t
|> map (fst o fst)
val (found_facts, lost_facts) =
flat proofs |> sort_distinct string_ord