--- 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), [])