--- a/src/HOL/TPTP/sledgehammer_tactics.ML Wed May 15 17:27:24 2013 +0200
+++ b/src/HOL/TPTP/sledgehammer_tactics.ML Wed May 15 17:43:42 2013 +0200
@@ -31,7 +31,7 @@
default_params ctxt override_params
val name = hd provers
val prover = get_prover ctxt mode name
- val default_max_facts = default_max_facts_for_prover ctxt slice name
+ val default_max_facts = default_max_facts_of_prover ctxt slice name
val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal i
val ho_atp = exists (is_ho_atp ctxt) provers
val reserved = reserved_isar_keyword_table ()