# HG changeset patch
# User desharna
# Date 1734536894 -3600
# Node ID 24c1edcbcc6b4c4c13f4ce7fca1ebf0290d8dcdd
# Parent  91a7e5719b2b365241780cbaf306d7286319af72# Parent  dee16531eaf0c5f57dc6104f518ba7f5d8c02e7f
merged

diff -r 91a7e5719b2b -r 24c1edcbcc6b src/HOL/Tools/ATP/atp_problem.ML
--- a/src/HOL/Tools/ATP/atp_problem.ML	Wed Dec 18 11:59:44 2024 +0100
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Wed Dec 18 16:48:14 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
diff -r 91a7e5719b2b -r 24c1edcbcc6b src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Wed Dec 18 11:59:44 2024 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Wed Dec 18 16:48:14 2024 +0100
@@ -145,7 +145,7 @@
     val prob_path =
       if problem_dest_dir = "" then
         File.tmp_path problem_file_name
-      else if File.exists (Path.explode problem_dest_dir) then
+      else if File.is_dir (Path.explode problem_dest_dir) then
         Path.explode problem_dest_dir + problem_file_name
       else
         error ("No such directory: " ^ quote problem_dest_dir)
@@ -233,9 +233,9 @@
               else
                   let val res = Isabelle_System.bash_process (Bash.script command |> Bash.redirect)
                   in Process_Result.out res end
-            (* Hackish: This removes the two first lines that contain call-specific information
-            such as timestamp. *)
-            val arg = cat_lines (drop 2 lines_of_atp_problem)
+            (* Hackish: This removes the first two lines that contain call-specific information
+            such as a timestamp. *)
+            val arg = cat_lines (command :: drop 2 lines_of_atp_problem)
           in
             Timing.timing (memoize_fun_call f) arg
           end
@@ -289,7 +289,7 @@
       let val proof_dest_dir_path = Path.explode proof_dest_dir in
         if proof_dest_dir = "" then
           Output.system_message "don't export proof"
-        else if File.exists proof_dest_dir_path then
+        else if File.is_dir proof_dest_dir_path then
           File.write (proof_dest_dir_path + proof_file_name) output
         else
           error ("No such directory: " ^ quote proof_dest_dir)