# HG changeset patch
# User wenzelm
# Date 1633556253 -7200
# Node ID bf34175e64dcea73bc3ad5a0ca41728eaba11459
# Parent  3984b1e91df69165b458ec94c2ecce0fe9fefcc9
tuned;

diff -r 3984b1e91df6 -r bf34175e64dc src/HOL/Tools/Nitpick/kodkod_sat.ML
--- a/src/HOL/Tools/Nitpick/kodkod_sat.ML	Wed Oct 06 23:21:21 2021 +0200
+++ b/src/HOL/Tools/Nitpick/kodkod_sat.ML	Wed Oct 06 23:37:33 2021 +0200
@@ -50,27 +50,23 @@
    ("SAT4J_Light", Internal (Java, Incremental, ["LightSAT4J"]))]
 
 fun dynamic_entry_for_external name dev home exec args markers =
-  case getenv home of
-    "" => NONE
-  | dir =>
-    SOME (name, fn () =>
-                   let
-                     val serial_str = serial_string ()
-                     val base = name ^ serial_str
-                     val out_file = base ^ ".out"
-                     val dir_sep =
-                       if String.isSubstring "\\" dir andalso
-                          not (String.isSubstring "/" dir) then
-                         "\\"
-                       else
-                         "/"
-                   in
-                     [if null markers then "External" else "ExternalV2",
-                      dir ^ dir_sep ^ exec, base ^ ".cnf"] @
-                      (if null markers then []
-                       else [if dev = ToFile then out_file else ""]) @ markers @
-                     (if dev = ToFile then [out_file] else []) @ args
-                   end)
+  let
+    fun make_args dir () =
+      let
+        val serial_str = serial_string ()
+        val base = name ^ serial_str
+        val out_file = base ^ ".out"
+        val dir_sep =
+          if String.isSubstring "\\" dir andalso not (String.isSubstring "/" dir)
+          then "\\" else "/"
+      in
+       [if null markers then "External" else "ExternalV2",
+        dir ^ dir_sep ^ exec, base ^ ".cnf"] @
+        (if null markers then []
+         else [if dev = ToFile then out_file else ""]) @ markers @
+       (if dev = ToFile then [out_file] else []) @ args
+      end
+  in case getenv home of "" => NONE | dir => SOME (name, make_args dir) end
 
 fun dynamic_entry_for_info incremental (name, Internal (Java, mode, ss)) =
     if incremental andalso mode = Batch then NONE else SOME (name, K ss)