--- a/src/HOL/TPTP/atp_problem_import.ML Fri Jan 31 16:07:20 2014 +0100
+++ b/src/HOL/TPTP/atp_problem_import.ML Fri Jan 31 16:10:39 2014 +0100
@@ -182,7 +182,7 @@
fun atp_tac ctxt completeness override_params timeout prover =
let
val ctxt =
- ctxt |> Config.put Sledgehammer_Prover.completish (completeness > 0)
+ ctxt |> Config.put Sledgehammer_Prover_ATP.atp_completish (completeness > 0)
fun ref_of th = (Facts.named (Thm.derivation_name th), [])
in
Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt