src/HOL/TPTP/atp_problem_import.ML

 fun atp_tac ctxt completeness override_params timeout assms prover =
   let
     val thy = Proof_Context.theory_of ctxt
     val assm_ths0 = map (Skip_Proof.make_thm thy) assms
     val ((assm_name, _), ctxt) = ctxt
-      |> Config.put Sledgehammer_Prover_ATP.atp_completish (completeness > 0)
+      |> Config.put Sledgehammer_Prover_ATP.atp_completish (if completeness > 0 then 2 else 0)
       |> Local_Theory.note ((@{binding thms}, []), assm_ths0)
 
     fun ref_of th = (Facts.named (Thm.derivation_name th), [])
     val ref_of_assms = (Facts.named assm_name, [])
   in