--- 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)