# HG changeset patch
# User desharna
# Date 1734536012 -3600
# Node ID dee16531eaf0c5f57dc6104f518ba7f5d8c02e7f
# Parent  6e09005f6ca8d22a56becc2873b7af5a59644bce
tuned ATP caching in Sledgehammer to consider the command line

diff -r 6e09005f6ca8 -r dee16531eaf0 src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Wed Dec 18 16:32:49 2024 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Wed Dec 18 16:33:32 2024 +0100
@@ -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