diff --git a/src/HOL/Tools/Nitpick/kodkod_sat.ML b/src/HOL/Tools/Nitpick/kodkod_sat.ML
--- a/src/HOL/Tools/Nitpick/kodkod_sat.ML
+++ b/src/HOL/Tools/Nitpick/kodkod_sat.ML
@@ -1,119 +1,115 @@
 (*  Title:      HOL/Tools/Nitpick/kodkod_sat.ML
     Author:     Jasmin Blanchette, TU Muenchen
     Copyright   2009, 2010
 
 Kodkod SAT solver integration.
 *)
 
 signature KODKOD_SAT =
 sig
   val configured_sat_solvers : bool -> string list
   val smart_sat_solver_name : bool -> string
   val sat_solver_spec : string -> string * string list
 end;
 
 structure Kodkod_SAT : KODKOD_SAT =
 struct
 
 open Kodkod
 
 datatype sink = ToStdout | ToFile
 datatype availability = Java | JNI of int list
 datatype mode = Batch | Incremental
 
 datatype sat_solver_info =
   Internal of availability * mode * string list |
   External of string * string * string list |
   ExternalV2 of sink * string * string * string list * string * string * string
 
 (* for compatibility with "SAT_Solver" *)
 val berkmin_exec = getenv "BERKMIN_EXE"
 
 val static_list =
   [("Lingeling_JNI", Internal (JNI [1, 5], Batch, ["Lingeling"])),
    ("CryptoMiniSat", External ("CRYPTOMINISAT_HOME", "cryptominisat", [])),
    ("CryptoMiniSat_JNI", Internal (JNI [1, 5], Batch, ["CryptoMiniSat"])),
    ("MiniSat", ExternalV2 (ToFile, "MINISAT_HOME", "minisat", [], "SAT", "", "UNSAT")),
    ("MiniSat_JNI", Internal (JNI [], Incremental, ["MiniSat"])),
    ("zChaff", ExternalV2 (ToStdout, "ZCHAFF_HOME", "zchaff", [],
                           "Instance Satisfiable", "",
                           "Instance Unsatisfiable")),
    ("RSat", ExternalV2 (ToStdout, "RSAT_HOME", "rsat", ["-s"],
                         "s SATISFIABLE", "v ", "s UNSATISFIABLE")),
    ("Riss3g", External ("RISS3G_HOME", "riss3g", [])),
    ("BerkMin", ExternalV2 (ToStdout, "BERKMIN_HOME",
                            if berkmin_exec = "" then "BerkMin561"
                            else berkmin_exec, [], "Satisfiable          !!",
                            "solution =", "UNSATISFIABLE          !!")),
    ("BerkMin_Alloy", External ("BERKMINALLOY_HOME", "berkmin", [])),
    ("SAT4J", Internal (Java, Incremental, ["DefaultSAT4J"])),
    ("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)
   | dynamic_entry_for_info incremental (name, Internal (JNI from_version, mode, ss)) =
     if (incremental andalso mode = Batch) orelse
        is_less (dict_ord int_ord (kodkodi_version (), from_version))
     then NONE
     else
       let
         val lib_paths = getenv "KODKODI_JAVA_LIBRARY_PATH" |> space_explode ":"
       in
         if exists (fn path => File.exists (Path.explode (path ^ "/"))) lib_paths
         then SOME (name, K ss)
         else NONE
       end
   | dynamic_entry_for_info false (name, External (home, exec, args)) =
     dynamic_entry_for_external name ToStdout home exec args []
   | dynamic_entry_for_info false
         (name, ExternalV2 (dev, home, exec, args, m1, m2, m3)) =
     dynamic_entry_for_external name dev home exec args [m1, m2, m3]
   | dynamic_entry_for_info true _ = NONE
 
 fun dynamic_list incremental =
   map_filter (dynamic_entry_for_info incremental) static_list
 
 val configured_sat_solvers = map fst o dynamic_list
 val smart_sat_solver_name = fst o hd o dynamic_list
 
 fun sat_solver_spec name =
   let
     val dyns = dynamic_list false
     fun enum_solvers solvers =
       commas (distinct (op =) (map (quote o fst) solvers))
   in
     (name, the (AList.lookup (op =) dyns name) ())
     handle Option.Option =>
            error (if AList.defined (op =) static_list name then
                     "The SAT solver " ^ quote name ^ " is not configured. The \
                     \following solvers are configured:\n" ^
                     enum_solvers dyns
                   else
                     "Unknown SAT solver " ^ quote name ^ "\nThe following \
                     \solvers are supported:\n" ^ enum_solvers static_list)
   end
 
 end;