diff -r a2e68976251f -r 6e09005f6ca8 src/HOL/Tools/ATP/atp_problem.ML --- a/src/HOL/Tools/ATP/atp_problem.ML Wed Dec 18 16:20:34 2024 +0100 +++ b/src/HOL/Tools/ATP/atp_problem.ML Wed Dec 18 16:32:49 2024 +0100 @@ -801,8 +801,8 @@ end fun lines_of_atp_problem format ord_info problem = - "% This file was generated by Isabelle (most likely Sledgehammer)\n\ - \% " ^ timestamp () ^ "\n" :: + "% This file was generated by Isabelle (most likely Sledgehammer)" :: + timestamp () :: (case format of DFG poly => dfg_lines poly ord_info | _ => tptp_lines format) problem