tuned tests for existing directories in Sledgehammer
authordesharna
Wed, 18 Dec 2024 16:20:34 +0100
changeset 81623 a2e68976251f
parent 81613 44afa6f1baad
child 81624 6e09005f6ca8
tuned tests for existing directories in Sledgehammer
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)