# HG changeset patch
# User wenzelm
# Date 1738704096 -3600
# Node ID 2028082805f00f094779e359be48d5427a5dc54a
# Parent  6d3938f1738d0f5245772c728e4c2c651e2cf3e5
tuned;

diff -r 6d3938f1738d -r 2028082805f0 src/HOL/Tools/SMT/smt_config.ML
--- a/src/HOL/Tools/SMT/smt_config.ML	Tue Feb 04 22:12:06 2025 +0100
+++ b/src/HOL/Tools/SMT/smt_config.ML	Tue Feb 04 22:21:36 2025 +0100
@@ -234,8 +234,8 @@
 fun select_certificates name context = context |> put_certificates (
   if name = "" then NONE
   else
-    (Resources.master_directory (Context.theory_of context) + Path.explode name)
-    |> SOME o Cache_IO.unsynchronized_init)
+    let val dir = Resources.master_directory (Context.theory_of context) + Path.explode name
+    in SOME (Cache_IO.unsynchronized_init dir) end);
 
 val setup_certificates =
   Attrib.setup \<^binding>\<open>smt_certificates\<close>