diff --git a/src/library/unification_hint.cpp b/src/library/unification_hint.cpp
index c39c28647d..431e650aa2 100644
--- a/src/library/unification_hint.cpp
+++ b/src/library/unification_hint.cpp
@@ -193,10 +193,15 @@ format unification_hint::pp(unsigned prio, formatter const & fmt) const {
     format r1 = fmt(get_lhs()) + space() + format("=?=") + pp_indent_expr(fmt, get_rhs());
     r1 += space() + lcurly();
     r += group(r1);
-    for_each(m_constraints, [&](expr_pair p) {
-            r += fmt(p.first) + space() + format("=?=");
-            r += space() + fmt(p.second) + comma() + space();
-        });
+    bool first = true;
+    for (expr_pair const & p : m_constraints) {
+        if (first) {
+            first = false;
+        } else {
+            r += comma() + space();
+        }
+        r += fmt(p.first) + space() + format("=?=") + space() + fmt(p.second);
+    }
     r += rcurly();
     return r;
 }
diff --git a/tests/lean/unification_hints1.lean.expected.out b/tests/lean/unification_hints1.lean.expected.out
index cf3972b128..a6d4dd11f5 100644
--- a/tests/lean/unification_hints1.lean.expected.out
+++ b/tests/lean/unification_hints1.lean.expected.out
@@ -5,11 +5,10 @@ unification hints:
 fail
 success
 unification hints:
-(add, nat.succ) #4 + 1 =?= succ #3 {#4 =?= #3, }
+(add, nat.succ) #4 + 1 =?= succ #3 {#4 =?= #3}
 fail
 success
 unification hints:
-(canonical.Canonical.carrier, canonical.A) Canonical.carrier #0 =?= A {#0 =?= A_canonical, }
+(canonical.Canonical.carrier, canonical.A) Canonical.carrier #0 =?= A {#0 =?= A_canonical}
 unification hints at namespace 'canonical':
-(canonical.Canonical.carrier, canonical.A) canonical.Canonical.carrier #0 =?=
-  canonical.A {#0 =?= canonical.A_canonical, }
+(canonical.Canonical.carrier, canonical.A) canonical.Canonical.carrier #0 =?= canonical.A {#0 =?= canonical.A_canonical}