diff --git a/src/library/tactic/congruence/congruence_closure.cpp b/src/library/tactic/congruence/congruence_closure.cpp
index 8fd8a254fd..a8bae49783 100644
--- a/src/library/tactic/congruence/congruence_closure.cpp
+++ b/src/library/tactic/congruence/congruence_closure.cpp
@@ -1287,10 +1287,10 @@ format congruence_closure::state::pp_eqcs(formatter const & fmt) const {
     format r;
     bool first = true;
     for (expr const & root : roots) {
-        if (first) first = false; r += line();
+        if (first) first = false; else r += comma() + line();
         r += pp_eqc(fmt, root);
     }
-    return r;
+    return bracket("{", group(r), "}");
 }
 
 void initialize_congruence_closure() {