--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Sun May 01 18:37:25 2011 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Sun May 01 18:37:25 2011 +0200
@@ -117,18 +117,18 @@
val default_max_relevant =
Sledgehammer_Provers.default_max_relevant_for_prover ctxt slicing
prover
- val is_built_in_const =
- Sledgehammer_Provers.is_built_in_const_for_prover ctxt default_prover
+ val is_built_in_const =
+ Sledgehammer_Provers.is_built_in_const_for_prover ctxt default_prover
val relevance_fudge =
extract_relevance_fudge args
(Sledgehammer_Provers.relevance_fudge_for_prover ctxt prover)
val relevance_override = {add = [], del = [], only = false}
val subgoal = 1
val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal subgoal
- val half_sound =
- Sledgehammer_Provers.is_rich_type_sys_half_sound type_sys
+ val fairly_sound =
+ Sledgehammer_Provers.is_rich_type_sys_fairly_sound type_sys
val facts =
- Sledgehammer_Filter.relevant_facts ctxt half_sound
+ Sledgehammer_Filter.relevant_facts ctxt fairly_sound
relevance_thresholds
(the_default default_max_relevant max_relevant) is_built_in_const
relevance_fudge relevance_override facts hyp_ts concl_t