diff -r 777328c9f1ea -r 1ee776da8da7 src/HOL/TPTP/atp_problem_import.ML
--- a/src/HOL/TPTP/atp_problem_import.ML	Fri Jan 31 10:23:32 2014 +0100
+++ b/src/HOL/TPTP/atp_problem_import.ML	Fri Jan 31 10:23:32 2014 +0100
@@ -182,7 +182,7 @@
 fun atp_tac ctxt completeness override_params timeout prover =
   let
     val ctxt =
-      ctxt |> Config.put Sledgehammer_Provers.completish (completeness > 0)
+      ctxt |> Config.put Sledgehammer_Prover.completish (completeness > 0)
     fun ref_of th = (Facts.named (Thm.derivation_name th), [])
   in
     Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt