# HG changeset patch
# User desharna
# Date 1734620466 -3600
# Node ID 362b2ff84206ea966a6c3fbc4879b52eb82cf153
# Parent  5617622681d74a43f2ebd59d17800482f6d0eb5b
minor performance tuning; directly try to read file instead of first checking its existence

diff -r 5617622681d7 -r 362b2ff84206 src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Thu Dec 19 08:26:04 2024 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Thu Dec 19 16:01:06 2024 +0100
@@ -494,23 +494,20 @@
     val hash = SHA1.rep (SHA1.digest arg)
     val file = cache_dir + Path.explode hash
   in
-    if File.is_file file then
+    (case try File.read file of
+      NONE => 
+      let val result = f arg in
+        File.write file result;
+        result
+      end
+    | SOME s =>
       let
         val () =
           if verbose then
             writeln ("Found problem with key " ^ hash ^ " in cache.")
           else
             ()
-      in
-        File.read file
-      end
-    else
-      let
-        val result = f arg
-      in
-        File.write file result;
-        result
-      end
+      in s end)
   end
 in