merged

--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Thu Dec 19 17:01:40 2024 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Thu Dec 19 17:01:54 2024 +0000
@@ -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