diff --git a/src/library/match.cpp b/src/library/match.cpp
index dca62d1f0..e69e144f2 100644
--- a/src/library/match.cpp
+++ b/src/library/match.cpp
@@ -352,7 +352,7 @@ bool match(expr const & p, expr const & t, buffer<optional<expr>> & esubst, buff
         return match_fn(esubst, lsubst, name_generator(*g_tmp_prefix), name_subst, plugin).match(p, t);
 }
 
-match_plugin mk_whnf_match_plugin(std::shared_ptr<type_checker> const & tc) {
+match_plugin mk_whnf_match_plugin(std::shared_ptr<type_checker> tc) {
     return [=](expr const & p, expr const & t, match_context & ctx) { // NOLINT
         try {
             constraint_seq cs;
diff --git a/src/library/match.h b/src/library/match.h
index 0fb08cffd..511b5eaf3 100644
--- a/src/library/match.h
+++ b/src/library/match.h
@@ -49,7 +49,7 @@ public:
 typedef std::function<bool(expr const &, expr const &, match_context &)> match_plugin; // NOLINT
 
 /** \brief Create a match_plugin that puts terms in weak-head-normal-form before failing */
-match_plugin mk_whnf_match_plugin(std::shared_ptr<type_checker> const & tc);
+match_plugin mk_whnf_match_plugin(std::shared_ptr<type_checker> tc);
 
 /**
    \brief Matching for higher-order patterns. Return true iff \c t matches the higher-order pattern \c p.