# HG changeset patch
# User blanchet
# Date 1504821712 -7200
# Node ID 7706577cd10e08119d2b63c7a8d88dfb9b106f92
# Parent  1f1c5d85d2328811d7b7a8bf3c959a8940d3f473
use proper syntax with nunchaku tool

diff -r 1f1c5d85d232 -r 7706577cd10e src/HOL/Tools/Nunchaku/nunchaku_tool.ML
--- a/src/HOL/Tools/Nunchaku/nunchaku_tool.ML	Fri Sep 08 00:01:36 2017 +0200
+++ b/src/HOL/Tools/Nunchaku/nunchaku_tool.ML	Fri Sep 08 00:01:52 2017 +0200
@@ -89,7 +89,7 @@
           "PATH=\"$CVC4_HOME:$KODKODI/bin:$PATH\" \"$" ^
           nunchaku_home_env_var ^ "\"/nunchaku --skolems-in-model --no-color " ^
           (if specialize then "" else "--no-specialize ") ^
-          "--solvers \"" ^ Bash_Syntax.string (space_implode " " solvers) ^ "\" " ^
+          "--solvers \"" ^ Bash_Syntax.string (space_implode "," solvers) ^ "\" " ^
           "--timeout " ^ string_of_int (Time.toSeconds timeout) ^ " " ^
           File.bash_path prob_path;
         val comments =