src/HOL/Tools/ATP_Manager/atp_wrapper.ML

                           higher_order follow_defs max_new_clauses
                           (the_default prefers_theory_relevant theory_relevant))
       (prepare_clauses higher_order false)
       (write_tptp_file (debug andalso overlord andalso not isar_proof)) command
       (arguments timeout) known_failures
-      (proof_text (supports_isar_proofs andalso isar_proof) modulus sorts)
+      (proof_text (supports_isar_proofs andalso isar_proof) debug modulus sorts)
       name params minimize_command
 
 fun tptp_prover name p = (name, generic_tptp_prover (name, p));