diff --git a/src/library/unifier.cpp b/src/library/unifier.cpp
index 0e3bb3b1c..3a9763908 100644
--- a/src/library/unifier.cpp
+++ b/src/library/unifier.cpp
@@ -1998,7 +1998,7 @@ struct unifier_fn {
         buffer<expr> lhs_args, rhs_args;
         expr ml = get_app_args(lhs, lhs_args);
         expr mr = get_app_args(rhs, rhs_args);
-        if (ml == mr) {
+        if (mlocal_name(ml) == mlocal_name(mr)) {
             discard(c);
             return true;
         }