diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index 968b2b2cbd..0f14533018 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -2538,7 +2538,6 @@ expr elaborator::visit_equation(expr const & e, unsigned num_fns) {
 }
 
 expr elaborator::visit_equations(expr const & e) {
-    expr const & ref = e;
     buffer<expr> eqs;
     buffer<expr> new_eqs;
     optional<expr> new_tacs;
@@ -2849,7 +2848,7 @@ class visit_structure_instance_fn {
                     fval = mk_app(default_val, args);
                     fval = head_beta_reduce(fval);
                 }
-                reduce_and_check_deps(fval, full_S_fname);
+                reduce_and_check_deps(fval);
                 return fval;
             }
         });
@@ -2975,7 +2974,7 @@ class visit_structure_instance_fn {
      * Also reduce projections containing mvars, which may remove dependencies.
      * Example: `functor.map (functor.mk ?p1 ?m1 ?m2...) => ?m1`
      */
-    void reduce_and_check_deps(expr & e, name const & full_S_fname) {
+    void reduce_and_check_deps(expr & e) {
         if (m_use_subobjects)
             e = reduce_projections_visitor(m_ctx)(e);
         name_set deps;
@@ -3053,7 +3052,7 @@ class visit_structure_instance_fn {
                     expr val;
 
                     try {
-                        reduce_and_check_deps(reduced_expected_type, full_S_fname);
+                        reduce_and_check_deps(reduced_expected_type);
                         /* note: we pass the reduced, mvar-free expected type. Otherwise auto params may fail with
                          * "result contains meta-variables". */
                         val = (*m_field2elab.find(S_fname))(reduced_expected_type);
diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp
index a1ed978af8..adc50ad8cc 100644
--- a/src/frontends/lean/pp.cpp
+++ b/src/frontends/lean/pp.cpp
@@ -463,13 +463,6 @@ auto pretty_fn::pp_child_core(expr const & e, unsigned bp, bool ignore_hide) ->
     return add_paren_if_needed(pp(e, ignore_hide), bp);
 }
 
-static expr consume_ref_annotations(expr const & e) {
-    if (is_explicit(e))
-        return consume_ref_annotations(get_explicit_arg(e));
-    else
-        return e;
-}
-
 static bool is_coercion(expr const & e) {
     return is_app_of(e, get_coe_name()) && get_app_num_args(e) >= 4;
 }
diff --git a/src/library/compiler/specialize.cpp b/src/library/compiler/specialize.cpp
index 911e7c5c7c..dfbbd637bc 100644
--- a/src/library/compiler/specialize.cpp
+++ b/src/library/compiler/specialize.cpp
@@ -460,7 +460,6 @@ class specialize_fn {
 
     /* Auxiliary class for collecting specialization dependencies. */
     class dep_collector {
-        type_checker::state & m_st;
         local_ctx             m_lctx;
         name_set              m_visited_not_in_binder;
         name_set              m_visited_in_binder;
@@ -572,8 +571,8 @@ class specialize_fn {
         }
 
     public:
-        dep_collector(type_checker::state & st, local_ctx const & lctx, spec_ctx & ctx):
-            m_st(st), m_lctx(lctx), m_ctx(ctx) {}
+        dep_collector(local_ctx const & lctx, spec_ctx & ctx):
+            m_lctx(lctx), m_ctx(ctx) {}
         void operator()(expr const & e) { return collect(e, false); }
     };
 
@@ -587,7 +586,7 @@ class specialize_fn {
         buffer<spec_arg_kind> kinds;
         get_arg_kinds(const_name(fn), kinds);
         bool has_attr   = has_specialize_attribute(env(), const_name(fn));
-        dep_collector collect(m_st, m_lctx, ctx);
+        dep_collector collect(m_lctx, ctx);
         unsigned sz     = std::min(kinds.size(), args.size());
         unsigned i      = sz;
         bool found_inst = false;