# HG changeset patch
# User desharna
# Date 1734535234 -3600
# Node ID a2e68976251fdee0e7c78e53b8c32bfe2f9de7cf
# Parent  44afa6f1baad90d9e8878136aba4359e3e8653c8
tuned tests for existing directories in Sledgehammer

diff -r 44afa6f1baad -r a2e68976251f src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Wed Dec 18 11:02:56 2024 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Wed Dec 18 16:20:34 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)
@@ -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)