# HG changeset patch
# User wenzelm
# Date 1613996995 -3600
# Node ID 10d3b49a702a6d15f63abd792a5a4669b323289f
# Parent  17c28251fff00434c471b12ffbccadfc180c25e6
tuned signature;

diff -r 17c28251fff0 -r 10d3b49a702a src/HOL/Tools/Nunchaku/nunchaku_tool.ML
--- a/src/HOL/Tools/Nunchaku/nunchaku_tool.ML	Mon Feb 22 12:30:05 2021 +0100
+++ b/src/HOL/Tools/Nunchaku/nunchaku_tool.ML	Mon Feb 22 13:29:55 2021 +0100
@@ -103,30 +103,30 @@
           [bash_cmd, "This file was generated by Isabelle (most likely Nunchaku)", timestamp ()];
         val prob_str = cat_lines (map (prefix "# ") comments) ^ "\n\n" ^ str_of_nun_problem problem;
         val _ = File.write prob_path prob_str;
-        val {out = output, err = error, rc = code, ...} = Isabelle_System.bash_process bash_cmd;
+        val {out, err, rc, ...} = Isabelle_System.bash_process bash_cmd;
 
         val backend =
-          (case map_filter (try (unprefix "{backend:")) (split_lines output) of
+          (case map_filter (try (unprefix "{backend:")) (split_lines out) of
             [s] => hd (space_explode "," s)
           | _ => unknown_solver);
       in
-        if String.isPrefix "SAT" output then
-          (if sound then Sat else Unknown o SOME) (backend, output, {tys = [], tms = []})
-        else if String.isPrefix "UNSAT" output then
+        if String.isPrefix "SAT" out then
+          (if sound then Sat else Unknown o SOME) (backend, out, {tys = [], tms = []})
+        else if String.isPrefix "UNSAT" out then
           if complete then Unsat backend else Unknown NONE
-        else if String.isSubstring "TIMEOUT" output
+        else if String.isSubstring "TIMEOUT" out
             (* FIXME: temporary *)
-            orelse String.isSubstring "kodkod failed (errcode 152)" error then
+            orelse String.isSubstring "kodkod failed (errcode 152)" err then
           Timeout
-        else if String.isPrefix "UNKNOWN" output then
+        else if String.isPrefix "UNKNOWN" out then
           Unknown NONE
-        else if code = 126 then
+        else if rc = 126 then
           Nunchaku_Cannot_Execute
-        else if code = 127 then
+        else if rc = 127 then
           Nunchaku_Not_Found
         else
-          Unknown_Error (code,
-            simplify_spaces (elide_string 1000 (if error <> "" then error else output)))
+          Unknown_Error (rc,
+            simplify_spaces (elide_string 1000 (if err <> "" then err else out)))
       end);
 
 fun solve_nun_problem (params as {solvers, overlord, debug, ...}) problem =