use right attribute separator in Nunchaku
authorblanchet
Fri, 08 Sep 2017 00:02:31 +0200
changeset 66629 d9ceebfba0af
parent 66628 a62c0c83feba
child 66630 034cabc4fda5
use right attribute separator in Nunchaku
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)) =