diff --git a/src/ast/rewriter/bool_rewriter.cpp b/src/ast/rewriter/bool_rewriter.cpp
index a9861093a..90e6c37d7 100644
--- a/src/ast/rewriter/bool_rewriter.cpp
+++ b/src/ast/rewriter/bool_rewriter.cpp
@@ -645,6 +645,11 @@ br_status bool_rewriter::try_ite_value(app * ite, app * val, expr_ref & result)
 }
 
 
+app* bool_rewriter::mk_eq(expr* lhs, expr* rhs) {
+    // if (lhs->get_id() > rhs->get_id()) std::swap(lhs, rhs);
+    return m().mk_eq(lhs, rhs);
+}
+
 br_status bool_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) {
     if (m().are_equal(lhs, rhs)) {
         result = m().mk_true();
diff --git a/src/ast/rewriter/bool_rewriter.h b/src/ast/rewriter/bool_rewriter.h
index 987c0a0eb..87f9d370d 100644
--- a/src/ast/rewriter/bool_rewriter.h
+++ b/src/ast/rewriter/bool_rewriter.h
@@ -127,10 +127,7 @@ public:
     br_status mk_ite_core(expr * c, expr * t, expr * e, expr_ref & result);
     br_status mk_not_core(expr * t, expr_ref & result);
 
-    app* mk_eq(expr* lhs, expr* rhs) {
-        if (lhs->get_id() > rhs->get_id()) std::swap(lhs, rhs);
-        return m().mk_eq(lhs, rhs);
-    }
+    app* mk_eq(expr* lhs, expr* rhs);
 
     void mk_eq(expr * lhs, expr * rhs, expr_ref & result) {
         if (mk_eq_core(lhs, rhs, result) == BR_FAILED)