--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed May 15 17:43:42 2013 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed May 15 17:49:18 2013 +0200
@@ -451,9 +451,9 @@
|> max_new_mono_instancesLST
|> max_mono_itersLST)
val default_max_facts =
- Sledgehammer_Provers.default_max_facts_for_prover ctxt slice prover_name
+ Sledgehammer_Provers.default_max_facts_of_prover ctxt slice prover_name
val is_appropriate_prop =
- Sledgehammer_Provers.is_appropriate_prop_for_prover ctxt prover_name
+ Sledgehammer_Provers.is_appropriate_prop_of_prover ctxt prover_name
val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal i
val time_limit =
(case hard_timeout of
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Wed May 15 17:43:42 2013 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Wed May 15 17:49:18 2013 +0200
@@ -116,13 +116,13 @@
val params as {max_facts, slice, ...} =
Sledgehammer_Isar.default_params ctxt args
val default_max_facts =
- Sledgehammer_Provers.default_max_facts_for_prover ctxt slice prover
+ Sledgehammer_Provers.default_max_facts_of_prover ctxt slice prover
val is_appropriate_prop =
- Sledgehammer_Provers.is_appropriate_prop_for_prover ctxt
+ Sledgehammer_Provers.is_appropriate_prop_of_prover ctxt
default_prover
val relevance_fudge =
extract_relevance_fudge args
- (Sledgehammer_Provers.relevance_fudge_for_prover ctxt prover)
+ (Sledgehammer_Provers.relevance_fudge_of_prover ctxt prover)
val subgoal = 1
val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal subgoal
val ho_atp = Sledgehammer_Provers.is_ho_atp ctxt prover