src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML

     end
 
     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)
 
     val executable =

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