diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index 4a272164a5..1321a8c9a8 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -483,7 +483,7 @@ class elaborator::imp {
         return process(e, ctx).second;
     }
 
-    bool is_simple_ho_match(expr const & e1, expr const & e2, context const & ctx) {
+    bool is_simple_ho_match(expr const & e1, context const & ctx) {
         if (is_app(e1) && is_metavar(arg(e1, 0)) && is_var(arg(e1, 1), 0) && num_args(e1) == 2 && !empty(ctx)) {
             return true;
         } else {
@@ -712,10 +712,10 @@ class elaborator::imp {
                     for (unsigned i = 0; i < num; i++) {
                         m_constraints.push_back(constraint(arg(new_lhs, i), arg(new_rhs, i), c));
                     }
-                } else if (is_simple_ho_match(new_lhs, new_rhs, c.m_ctx)) {
+                } else if (is_simple_ho_match(new_lhs, c.m_ctx)) {
                     delayed = 0;
                     unify_simple_ho_match(new_lhs, new_rhs, c);
-                } else if (is_simple_ho_match(new_rhs, new_lhs, c.m_ctx)) {
+                } else if (is_simple_ho_match(new_rhs, c.m_ctx)) {
                     delayed = 0;
                     unify_simple_ho_match(new_rhs, new_lhs, c);
                 } else if (has_assigned_metavar(new_lhs)) {
diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index 0a410476f6..5c29ae1c07 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -708,7 +708,10 @@ class parser::imp {
         buffer<std::pair<pos_info, name>> names;
         parse_names(names);
         expr type;
-        if (curr_is_colon()) {
+        if (!suppress_type) {
+            check_colon_next("invalid binder, ':' expected");
+            type = parse_expr();
+        } else if (curr_is_colon()) {
             next();
             type = parse_expr();
         }
diff --git a/src/kernel/normalizer.cpp b/src/kernel/normalizer.cpp
index a876851f03..c4da9f21f4 100644
--- a/src/kernel/normalizer.cpp
+++ b/src/kernel/normalizer.cpp
@@ -97,7 +97,7 @@ class normalizer::imp {
         }
     };
 
-    svalue lookup(value_stack const & s, unsigned i, unsigned k) {
+    svalue lookup(value_stack const & s, unsigned i) {
         unsigned j = i;
         value_stack const * it1 = &s;
         while (*it1) {
@@ -202,7 +202,7 @@ class normalizer::imp {
             }
             break;
         case expr_kind::Var:
-            r = lookup(s, var_idx(a), k);
+            r = lookup(s, var_idx(a));
             break;
         case expr_kind::Constant: {
             object const & obj = m_env.get_object(const_name(a));
diff --git a/src/library/ho_unifier.cpp b/src/library/ho_unifier.cpp
index d478787152..b054d3be99 100644
--- a/src/library/ho_unifier.cpp
+++ b/src/library/ho_unifier.cpp
@@ -285,12 +285,12 @@ class ho_unifier::imp {
     }
 
     /** \brief Creates a subproblem based on the application arguments */
-    bool process_app_args(context const & ctx, expr const & a, expr const & b, unsigned) {
+    bool process_app_args(context const & ctx, expr const & a, expr const & b, unsigned start) {
         lean_assert(is_app(a) && is_app(b));
         if (num_args(a) != num_args(b)) {
             return false;
         } else {
-            for (unsigned i = 1; i < num_args(a); i++) {
+            for (unsigned i = start; i < num_args(a); i++) {
                 add_constraint(ctx, arg(a, i), arg(b, i));
             }
             return true;