tuned;
authorwenzelm
Tue, 04 Feb 2025 22:21:36 +0100
changeset 82079 2028082805f0
parent 82078 6d3938f1738d
child 82080 0aa2d1c132b2
child 82082 794bf73e100f
child 82104 90e10664e9f7
tuned;
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>