diff -r 8adf274f5988 -r 27333dc58e28 src/HOL/TPTP/atp_problem_import.ML
--- a/src/HOL/TPTP/atp_problem_import.ML	Sat Mar 26 18:51:58 2016 +0100
+++ b/src/HOL/TPTP/atp_problem_import.ML	Mon Mar 28 12:05:47 2016 +0200
@@ -185,7 +185,7 @@
     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), [])