src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML

                   in
                     (verbose, (metis_type_enc, metis_lam_trans), preplay_timeout, compress, try0,
                      minimize, atp_proof, goal)
                   end
 
-                val one_line_params =
-                  (preplay, proof_banner mode name, used_facts, subgoal, subgoal_count)
+                val one_line_params = (preplay, proof_banner mode name, subgoal, subgoal_count)
                 val num_chained = length (#facts (Proof.goal state))
               in
                 proof_text ctxt debug isar_proofs smt_proofs isar_params num_chained
                   one_line_params ^
                 (if important_message <> "" then