--- a/src/HOL/Tools/Nitpick/kodkod.ML Tue Sep 29 11:15:51 2020 +0200
+++ b/src/HOL/Tools/Nitpick/kodkod.ML Tue Sep 29 11:35:21 2020 +0200
@@ -158,7 +158,6 @@
datatype outcome =
JavaNotFound |
- KodkodiNotInstalled |
Normal of (int * raw_bound list) list * int list * string |
TimedOut of int list |
Error of string * int list
@@ -304,7 +303,6 @@
datatype outcome =
JavaNotFound |
- KodkodiNotInstalled |
Normal of (int * raw_bound list) list * int list * string |
TimedOut of int list |
Error of string * int list
@@ -1057,9 +1055,6 @@
perhaps (try (unprefix "Error: ")))
|> find_first (fn line => line <> "" andalso line <> "EXIT")
|> the_default ""
- fun has_error s =
- first_error |> Substring.full |> Substring.position s |> snd
- |> Substring.isEmpty |> not
in
if null ps then
if rc = 130 then
@@ -1070,8 +1065,6 @@
Normal ([], js, first_error)
else if rc = 127 then
JavaNotFound
- else if has_error "NoClassDefFoundError" then
- KodkodiNotInstalled
else if first_error <> "" then
Error (first_error, js)
else