diff --git a/src/kernel/expr_eq_fn.cpp b/src/kernel/expr_eq_fn.cpp
index 90ff8491e..bdce8c24a 100644
--- a/src/kernel/expr_eq_fn.cpp
+++ b/src/kernel/expr_eq_fn.cpp
@@ -92,6 +92,7 @@ class expr_eq_fn {
             return
                 apply(binding_domain(a), binding_domain(b)) &&
                 apply(binding_body(a), binding_body(b)) &&
+                (!CompareBinderInfo || binding_name(a) == binding_name(b)) &&
                 (!CompareBinderInfo || binding_info(a) == binding_info(b));
         case expr_kind::Sort:
             return sort_level(a) == sort_level(b);
diff --git a/src/tests/kernel/max_sharing.cpp b/src/tests/kernel/max_sharing.cpp
index 0f2bac585..16fe929e7 100644
--- a/src/tests/kernel/max_sharing.cpp
+++ b/src/tests/kernel/max_sharing.cpp
@@ -28,7 +28,7 @@ static void tst1() {
     lean_assert(!is_eqp(app_arg(app_fn(F1)), app_arg(F1)));
     F2 = max_fn(F1);
     std::cout << F2 << "\n";
-    lean_assert(is_eqp(app_arg(app_fn(F2)), app_arg(F2)));
+    lean_assert(!is_eqp(app_arg(app_fn(F2)), app_arg(F2))); // name matter
     max_fn.clear();
 }
 
diff --git a/tests/lean/congr1.lean.expected.out b/tests/lean/congr1.lean.expected.out
index 9d956c934..e6910def5 100644
--- a/tests/lean/congr1.lean.expected.out
+++ b/tests/lean/congr1.lean.expected.out
@@ -1,7 +1,7 @@
 [fixed, fixed, eq, eq]
-λ (A : Type) (c : has_add A) (a a_1 : A) (e_3 : a = a_1) (a_2 a_3 : A) (e_4 : a_2 = a_3), congr (congr_arg add e_3) e_4
+λ (A : Type) (s : has_add A) (a a_1 : A) (e_3 : a = a_1) (a_2 a_3 : A) (e_4 : a_2 = a_3), congr (congr_arg add e_3) e_4
 :
-∀ (A : Type) (c : has_add A) (a a_1 : A), a = a_1 → (∀ (a_2 a_3 : A), a_2 = a_3 → a + a_2 = a_1 + a_3)
+∀ (A : Type) (s : has_add A) (a a_1 : A), a = a_1 → (∀ (a_2 a_3 : A), a_2 = a_3 → a + a_2 = a_1 + a_3)
 [eq, cast, fixed, eq, eq]
 λ (c c_1 : Prop) (e_1 : c = c_1) (H : decidable c) (A : Type) (t t_1 : A) (e_4 : t = t_1) (e e_2 : A) (e_5 : e = e_2),
   eq.drec (eq.drec (eq.drec (eq.refl (ite c t e)) e_5) e_4) e_1
diff --git a/tests/lean/congr2.lean.expected.out b/tests/lean/congr2.lean.expected.out
index d4e797aac..953b24352 100644
--- a/tests/lean/congr2.lean.expected.out
+++ b/tests/lean/congr2.lean.expected.out
@@ -1,7 +1,7 @@
 [fixed, fixed, eq, eq]
-λ (A : Type) (c : has_add A) (a a_1 : A) (e_3 : a = a_1) (a_2 a_3 : A) (e_4 : a_2 = a_3), congr (congr_arg add e_3) e_4
+λ (A : Type) (s : has_add A) (a a_1 : A) (e_3 : a = a_1) (a_2 a_3 : A) (e_4 : a_2 = a_3), congr (congr_arg add e_3) e_4
 :
-∀ (A : Type) (c : has_add A) (a a_1 : A), a = a_1 → (∀ (a_2 a_3 : A), a_2 = a_3 → a + a_2 = a_1 + a_3)
+∀ (A : Type) (s : has_add A) (a a_1 : A), a = a_1 → (∀ (a_2 a_3 : A), a_2 = a_3 → a + a_2 = a_1 + a_3)
 [fixed, eq, eq]
 λ (A : Type) (a a_1 : list A) (e_2 : a = a_1) (a_2 a_3 : list A) (e_3 : a_2 = a_3), congr (congr_arg perm e_2) e_3
 :
diff --git a/tests/lean/extra/print_info.12.19.expected.out b/tests/lean/extra/print_info.12.19.expected.out
index 1cc9c1427..218756949 100644
--- a/tests/lean/extra/print_info.12.19.expected.out
+++ b/tests/lean/extra/print_info.12.19.expected.out
@@ -1,3 +1,3 @@
 LEAN_INFORMATION
-definition mul : Π {A : Type} [c : has_mul A], A → A → A
+definition mul : Π {A : Type} [s : has_mul A], A → A → A
 END_LEAN_INFORMATION
diff --git a/tests/lean/extra/print_info.12.20.expected.out b/tests/lean/extra/print_info.12.20.expected.out
index 1cc9c1427..218756949 100644
--- a/tests/lean/extra/print_info.12.20.expected.out
+++ b/tests/lean/extra/print_info.12.20.expected.out
@@ -1,3 +1,3 @@
 LEAN_INFORMATION
-definition mul : Π {A : Type} [c : has_mul A], A → A → A
+definition mul : Π {A : Type} [s : has_mul A], A → A → A
 END_LEAN_INFORMATION
diff --git a/tests/lean/extra/print_info.7.18.expected.out b/tests/lean/extra/print_info.7.18.expected.out
index 24056b2ae..e5417a85a 100644
--- a/tests/lean/extra/print_info.7.18.expected.out
+++ b/tests/lean/extra/print_info.7.18.expected.out
@@ -1,3 +1,3 @@
 LEAN_INFORMATION
-definition add : Π {A : Type} [c : has_add A], A → A → A
+definition add : Π {A : Type} [s : has_add A], A → A → A
 END_LEAN_INFORMATION