--- 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)