diff --git a/src/library/definitional/equations.cpp b/src/library/definitional/equations.cpp
index 1984ce2c0..20aa143b7 100644
--- a/src/library/definitional/equations.cpp
+++ b/src/library/definitional/equations.cpp
@@ -467,6 +467,8 @@ class equation_compiler_fn {
         for (expr const & fn : m_fns) {
             buffer<expr> args;
             expr r_type       = to_telescope(mlocal_type(fn), args);
+            for (expr & arg : args)
+                arg = update_mlocal(arg, whnf(mlocal_type(arg)));
             list<expr> ctx    = to_list(args);
             list<optional<name>> vstack = map2<optional<name>>(ctx, [](expr const & e) {
                     return optional<name>(mlocal_name(e));
diff --git a/tests/lean/run/eq25.lean b/tests/lean/run/eq25.lean
new file mode 100644
index 000000000..823ac0e6d
--- /dev/null
+++ b/tests/lean/run/eq25.lean
@@ -0,0 +1,11 @@
+inductive N :=
+O : N,
+S : N → N
+
+definition Nat := N
+
+open N
+
+definition add : Nat → Nat → Nat,
+add O     b := b,
+add (S a) b := S (add a b)