diff --git a/src/kernel/metavar.cpp b/src/kernel/metavar.cpp
index dc1284aa98..66dde3469f 100644
--- a/src/kernel/metavar.cpp
+++ b/src/kernel/metavar.cpp
@@ -51,13 +51,6 @@ public:
     virtual optional<expr> get_main_expr() const { return some_expr(m_expr); }
 };
 
-void swap(metavar_env & a, metavar_env & b) {
-    swap(a.m_name_generator,         b.m_name_generator);
-    swap(a.m_metavar_data,           b.m_metavar_data);
-    std::swap(a.m_beta_reduce_mv,    b.m_beta_reduce_mv);
-    std::swap(a.m_timestamp,         b.m_timestamp);
-}
-
 void metavar_env::inc_timestamp() {
     if (m_timestamp == std::numeric_limits<unsigned>::max()) {
         // This should not happen in real examples. We add it just to be safe.
diff --git a/src/kernel/metavar.h b/src/kernel/metavar.h
index e7363a2970..12c39180e8 100644
--- a/src/kernel/metavar.h
+++ b/src/kernel/metavar.h
@@ -154,8 +154,6 @@ public:
     }
 };
 
-void swap(metavar_env & a, metavar_env & b);
-
 /**
    \brief Apply the changes in \c lctx to \c a.
 */