remove special cases for CVC4 that are actually unused (see also 6273d4c8325b and 1f1c5d85d232);
--- a/src/HOL/Tools/Nunchaku/nunchaku.ML Wed Jan 08 14:30:17 2025 +0100
+++ b/src/HOL/Tools/Nunchaku/nunchaku.ML Wed Jan 08 14:35:30 2025 +0100
@@ -277,9 +277,6 @@
(print_n "External tool \"nunchaku\" cannot execute"; (unknownN, NONE))
| Nunchaku_Not_Found =>
(print_n "External tool \"nunchaku\" not found"; (unknownN, NONE))
- | CVC4_Cannot_Execute =>
- (print_n "External tool \"cvc4\" cannot execute"; (unknownN, NONE))
- | CVC4_Not_Found => (print_n "External tool \"cvc4\" not found"; (unknownN, NONE))
| Unknown_Error (code, msg) =>
(print_n ("Error: " ^ unprefix_error msg ^
(if code = 0 then "" else " (code " ^ string_of_int code ^ ")"));
--- a/src/HOL/Tools/Nunchaku/nunchaku_tool.ML Wed Jan 08 14:30:17 2025 +0100
+++ b/src/HOL/Tools/Nunchaku/nunchaku_tool.ML Wed Jan 08 14:35:30 2025 +0100
@@ -33,8 +33,6 @@
| Nunchaku_Var_Not_Set
| Nunchaku_Cannot_Execute
| Nunchaku_Not_Found
- | CVC4_Cannot_Execute
- | CVC4_Not_Found
| Unknown_Error of int * string
val nunchaku_home_env_var: string
@@ -70,8 +68,6 @@
| Nunchaku_Var_Not_Set
| Nunchaku_Cannot_Execute
| Nunchaku_Not_Found
-| CVC4_Cannot_Execute
-| CVC4_Not_Found
| Unknown_Error of int * string;
val nunchaku_home_env_var = "NUNCHAKU_HOME";