# HG changeset patch
# User wenzelm
# Date 1511947962 -3600
# Node ID 66fda545327f6dec31b50346677b4d223673c8d0
# Parent  05ff3e6dbbce8566479a82feb98bb22e2a2ab2d7
tuned;

diff -r 05ff3e6dbbce -r 66fda545327f src/HOL/Tools/Nunchaku/nunchaku_tool.ML
--- a/src/HOL/Tools/Nunchaku/nunchaku_tool.ML	Wed Nov 29 10:27:56 2017 +0100
+++ b/src/HOL/Tools/Nunchaku/nunchaku_tool.ML	Wed Nov 29 10:32:42 2017 +0100
@@ -98,7 +98,7 @@
           "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_Syntax.string solvers) ^ "\" " ^
+          "--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 ^ " ") ^