# HG changeset patch
# User wenzelm
# Date 1633639458 -7200
# Node ID d219a959b951e68175eb2c18f523dd28aae12a8e
# Parent  13b74f2e1f96c4d2ae8cf424809eb0683a4e1d14
clarified test of directories;

diff -r 13b74f2e1f96 -r d219a959b951 src/HOL/Tools/Nitpick/kodkod_sat.ML
--- a/src/HOL/Tools/Nitpick/kodkod_sat.ML	Thu Oct 07 22:21:11 2021 +0200
+++ b/src/HOL/Tools/Nitpick/kodkod_sat.ML	Thu Oct 07 22:44:18 2021 +0200
@@ -66,14 +66,8 @@
     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
+    else if exists File.is_dir (Path.split (getenv "KODKODI_JAVA_LIBRARY_PATH"))
+    then SOME (name, K ss) else NONE
   | dynamic_entry_for_info false (name, External (home, exec, args)) =
     dynamic_entry_for_external name ToStdout home exec args []
   | dynamic_entry_for_info false