diff --git a/src/HOL/Tools/Nunchaku/nunchaku_tool.ML b/src/HOL/Tools/Nunchaku/nunchaku_tool.ML
--- a/src/HOL/Tools/Nunchaku/nunchaku_tool.ML
+++ b/src/HOL/Tools/Nunchaku/nunchaku_tool.ML
@@ -1,153 +1,153 @@
 (*  Title:      HOL/Tools/Nunchaku/nunchaku_tool.ML
     Author:     Jasmin Blanchette, VU Amsterdam
     Copyright   2015, 2016, 2017
 
 Interface to the external "nunchaku" tool.
 *)
 
 signature NUNCHAKU_TOOL =
 sig
   type ty = Nunchaku_Problem.ty
   type tm = Nunchaku_Problem.tm
   type nun_problem = Nunchaku_Problem.nun_problem
 
   type tool_params =
     {solvers: string list,
      overlord: bool,
      min_bound: int,
      max_bound: int option,
      bound_increment: int,
      debug: bool,
      specialize: bool,
      timeout: Time.time}
 
   type nun_solution =
     {tys: (ty * tm list) list,
      tms: (tm * tm) list}
 
   datatype nun_outcome =
     Unsat of string
   | Sat of string * string * nun_solution
   | Unknown of (string * string * nun_solution) option
   | Timeout
   | 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
 
   val solve_nun_problem: tool_params -> nun_problem -> nun_outcome
 end;
 
 structure Nunchaku_Tool : NUNCHAKU_TOOL =
 struct
 
 open Nunchaku_Util;
 open Nunchaku_Problem;
 
 type tool_params =
   {solvers: string list,
    overlord: bool,
    min_bound: int,
    max_bound: int option,
    bound_increment: int,
    debug: bool,
    specialize: bool,
    timeout: Time.time};
 
 type nun_solution =
   {tys: (ty * tm list) list,
    tms: (tm * tm) list};
 
 datatype nun_outcome =
   Unsat of string
 | Sat of string * string * nun_solution
 | Unknown of (string * string * nun_solution) option
 | Timeout
 | 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";
 
 val unknown_solver = "unknown";
 
 val cached_outcome = Synchronized.var "Nunchaku_Tool.cached_outcome"
   (NONE : ((tool_params * nun_problem) * nun_outcome) option);
 
 fun uncached_solve_nun_problem ({solvers, overlord, min_bound, max_bound, bound_increment,
       specialize, timeout, ...} : tool_params)
     (problem as {sound, complete, ...}) =
   with_tmp_or_overlord_file overlord "nunchaku" "nun" (fn prob_path =>
     if getenv nunchaku_home_env_var = "" then
       Nunchaku_Var_Not_Set
     else
       let
         val bash_cmd =
           "PATH=\"$CVC4_HOME:$KODKODI/bin:$SMBC_HOME:$PATH\" \"$" ^
           nunchaku_home_env_var ^ "\"/nunchaku --skolems-in-model --no-color " ^
           (if specialize then "" else "--no-specialize ") ^
           "--solvers \"" ^ space_implode "," (map Bash.string solvers) ^ "\" " ^
           "--timeout " ^ string_of_int (Time.toSeconds timeout) ^ " " ^
           "--kodkod-min-bound " ^ string_of_int min_bound ^ " " ^
           (case max_bound of NONE => "" | SOME n => "--kodkod-max-bound " ^ string_of_int n ^ " ") ^
           "--kodkod-bound-increment " ^ string_of_int bound_increment ^ " " ^
           File.bash_path prob_path;
         val comments =
           [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 =
   let val key = (params, problem) in
     (case (overlord orelse debug,
         AList.lookup (op =) (the_list (Synchronized.value cached_outcome)) key) of
       (false, SOME outcome) => outcome
     | _ =>
       let
         val outcome = uncached_solve_nun_problem params problem;
 
         fun update_cache () =
           Synchronized.change cached_outcome (K (SOME (key, outcome)));
       in
         (case outcome of
           Unsat _ => update_cache ()
         | Sat _ => update_cache ()
         | Unknown _ => update_cache ()
         | _ => ());
         outcome
       end)
   end;
 
 end;