diff --git a/library/Init/Lean/Meta/ExprDefEq.lean b/library/Init/Lean/Meta/ExprDefEq.lean
index 4de74e6134..f48a70645e 100644
--- a/library/Init/Lean/Meta/ExprDefEq.lean
+++ b/library/Init/Lean/Meta/ExprDefEq.lean
@@ -322,7 +322,9 @@ do lctx ← getLCtx;
    and all examples we have identified are in Init/Control.
 
  A3) `a₁ ... aₙ` are not pairwise distinct (failed condition 1).
-   We can approximate again, but the limitations are very similar to the previous one.
+   In Lean3, we would try to approximate this case using an approach similar to A2.
+   However, this approximation complicates the code, and is never used in the
+   Lean3 stdlib and mathlib.
 
  A4) `t` contains a metavariable `?m'@C'` where `C'` is not a subprefix of `C`.
    (approximated) solution: restrict the context of `?m'`
diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp
index 6a69340664..e02600368e 100644
--- a/src/library/type_context.cpp
+++ b/src/library/type_context.cpp
@@ -1869,11 +1869,7 @@ bool type_context_old::process_assignment(expr const & m, expr const & v) {
         } else {
             if (std::any_of(locals.begin(), locals.end(),
                             [&](expr const & local) { return local_name(local) == local_name(arg); })) {
-                /* m is of the form (?M ... l ... l ...) where l is a local constant. */
-                if (quasi_pattern_unif_approx()) {
-                    /* workaround A3 */
-                    add_locals = false;
-                } else if (fo_unif_approx()) {
+                if (fo_unif_approx()) {
                     use_fo     = true;
                     add_locals = false;
                 } else {