# HG changeset patch
# User blanchet
# Date 1504821751 -7200
# Node ID d9ceebfba0af3bf8edb7b5e72fda27f97894870f
# Parent  a62c0c83feba57d55e7b8b904b86c7f6d92b88db
use right attribute separator in Nunchaku

diff -r a62c0c83feba -r d9ceebfba0af src/HOL/Tools/Nunchaku/nunchaku_problem.ML
--- a/src/HOL/Tools/Nunchaku/nunchaku_problem.ML	Fri Sep 08 00:02:31 2017 +0200
+++ b/src/HOL/Tools/Nunchaku/nunchaku_problem.ML	Fri Sep 08 00:02:31 2017 +0200
@@ -744,7 +744,7 @@
       val s1 = Option.map (prefix "min_card " o signed_string_of_int) c1;
       val s2 = Option.map (prefix "max_card " o signed_string_of_int) c2;
     in
-      enclose " [" "]" (space_implode ", " (map_filter I [s1, s2]))
+      enclose " [" "]" (space_implode "; " (map_filter I [s1, s2]))
     end;
 
 fun str_of_nun_command (NTVal (ty, cards)) =