# HG changeset patch
# User desharna
# Date 1734592701 -3600
# Node ID 5d401684b0837485f11570009f9dbbe5bc710e63
# Parent  24c1edcbcc6b4c4c13f4ce7fca1ebf0290d8dcdd
minor performance tuning; avoid constructing path if unused and double construction

diff -r 24c1edcbcc6b -r 5d401684b083 src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Wed Dec 18 16:48:14 2024 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Thu Dec 19 08:18:21 2024 +0100
@@ -145,10 +145,13 @@
     val prob_path =
       if problem_dest_dir = "" then
         File.tmp_path problem_file_name
-      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)
+        let val problem_dest_dir_path = Path.explode problem_dest_dir in
+          if File.is_dir problem_dest_dir_path then
+            problem_dest_dir_path + problem_file_name
+          else
+            error ("No such directory: " ^ quote problem_dest_dir)
+        end
 
     val executable =
       (case find_first (fn var => getenv var <> "") (fst exec) of
@@ -286,14 +289,15 @@
        too. *)
     fun clean_up () = if problem_dest_dir = "" then (try File.rm prob_path; ()) else ()
     fun export (_, (output, _, _, _, _, _, _, _), _) =
-      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.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)
-      end
+      if proof_dest_dir = "" then
+        Output.system_message "don't export proof"
+      else
+        let val proof_dest_dir_path = Path.explode proof_dest_dir in
+          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)
+        end
 
     val ((_, pool, lifted, sym_tab),
          (_, run_time, used_from, atp_problem, tstplike_proof, atp_proof,