diff --git a/src/kernel/metavar.cpp b/src/kernel/metavar.cpp
index 40f9763c2..cd14e775e 100644
--- a/src/kernel/metavar.cpp
+++ b/src/kernel/metavar.cpp
@@ -337,7 +337,7 @@ name_set substitution::get_occs(name const & m, name_set & fresh) {
     }
 }
 
-bool substitution::occurs_expr(name const & m, expr const & e) const {
+bool substitution::occurs_expr(name const & m, expr const & e) {
     if (!has_expr_metavar(e))
         return false;
     name_set fresh;
diff --git a/src/kernel/metavar.h b/src/kernel/metavar.h
index fb06669fa..882555dd7 100644
--- a/src/kernel/metavar.h
+++ b/src/kernel/metavar.h
@@ -105,7 +105,7 @@ public:
     optional<level> get_level(level const & m) const { lean_assert(is_meta(m)); return get_level(meta_id(m)); }
 
     /** \brief Return true iff the metavariable \c m occurrs (directly or indirectly) in \c e. */
-    bool occurs_expr(name const & m, expr const & e) const;
-    bool occurs(expr const & m, expr const & e) const { lean_assert(is_metavar(m)); return occurs_expr(mlocal_name(m), e); }
+    bool occurs_expr(name const & m, expr const & e);
+    bool occurs(expr const & m, expr const & e) { lean_assert(is_metavar(m)); return occurs_expr(mlocal_name(m), e); }
 };
 }