# HG changeset patch
# User blanchet
# Date 1504821772 -7200
# Node ID 6950d3da13f8c490dbe1b993a4bbd4f8c09a3afc
# Parent  c275542d6838d2fdd204875d6e8f2d8c314e05b2
rephrased error

diff -r c275542d6838 -r 6950d3da13f8 src/HOL/Tools/Nunchaku/nunchaku.ML
--- a/src/HOL/Tools/Nunchaku/nunchaku.ML	Fri Sep 08 00:02:48 2017 +0200
+++ b/src/HOL/Tools/Nunchaku/nunchaku.ML	Fri Sep 08 00:02:52 2017 +0200
@@ -281,7 +281,7 @@
               (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 ("Unknown error: " ^ unprefix_error msg ^
+              (print_n ("Error: " ^ unprefix_error msg ^
                  (if code = 0 then "" else " (code " ^ string_of_int code ^ ")"));
                (unknownN, NONE)))
           end