diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp
index 078cc7b7b4..0742904683 100644
--- a/src/frontends/lean/builtin_exprs.cpp
+++ b/src/frontends/lean/builtin_exprs.cpp
@@ -227,7 +227,7 @@ static expr parse_begin_end_core(parser & p, pos_info const & start_pos,
                 expr assert_tac = p.save_pos(mk_assert_tactic_expr(id, A), pos);
                 tacs.push_back(mk_begin_end_element_annotation(assert_tac));
                 if (p.curr_is_token(get_bar_tk())) {
-                    expr local = p.save_pos(mk_local(id, A), id_pos);
+                    expr local = p.save_pos(mk_local(id, A, mk_rec_info(true)), id_pos);
                     expr t     = parse_local_equations(p, local);
                     t      = p.mk_app(get_rexact_tac_fn(), t, pos);
                     t      = p.save_pos(mk_begin_end_element_annotation(t), pos);
@@ -438,7 +438,7 @@ static expr parse_have_core(parser & p, pos_info const & pos, optional<expr> con
     }
     expr proof;
     if (p.curr_is_token(get_bar_tk()) && !prev_local) {
-        expr fn = p.save_pos(mk_local(id, prop), id_pos);
+        expr fn = p.save_pos(mk_local(id, prop, mk_rec_info(true)), id_pos);
         proof = parse_local_equations(p, fn);
     } else {
         p.check_token_next(get_comma_tk(), "invalid 'have/assert' declaration, ',' expected");
@@ -521,7 +521,7 @@ static expr parse_suppose(parser & p, unsigned, expr const *, pos_info const & p
 static expr parse_show(parser & p, unsigned, expr const *, pos_info const & pos) {
     expr prop  = p.parse_expr();
     if (p.curr_is_token(get_bar_tk())) {
-        expr fn = p.save_pos(mk_local(get_this_tk(), prop), pos);
+        expr fn = p.save_pos(mk_local(get_this_tk(), prop, mk_rec_info(true)), pos);
         return parse_local_equations(p, fn);
     } else {
         p.check_token_next(get_comma_tk(), "invalid 'show' declaration, ',' expected");
diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp
index 8d4e10eaa8..4cf8f04561 100644
--- a/src/frontends/lean/decl_cmds.cpp
+++ b/src/frontends/lean/decl_cmds.cpp
@@ -604,7 +604,7 @@ expr parse_equations(parser & p, name const & n, expr const & type, buffer<name>
         for (expr const & param : ps)
             p.add_local(param);
         lean_assert(is_curr_with_or_comma_or_bar(p));
-        fns.push_back(mk_local(n, type));
+        fns.push_back(mk_local(n, type, mk_rec_info(true)));
         if (p.curr_is_token(get_with_tk())) {
             while (p.curr_is_token(get_with_tk())) {
                 p.next();
@@ -612,7 +612,7 @@ expr parse_equations(parser & p, name const & n, expr const & type, buffer<name>
                 name g_name = p.check_decl_id_next("invalid declaration, identifier expected");
                 p.check_token_next(get_colon_tk(), "invalid declaration, ':' expected");
                 expr g_type = p.parse_expr();
-                expr g      = p.save_pos(mk_local(g_name, g_type), pos);
+                expr g      = p.save_pos(mk_local(g_name, g_type, mk_rec_info(true)), pos);
                 auxs.push_back(g_name);
                 fns.push_back(g);
             }
diff --git a/src/kernel/expr.h b/src/kernel/expr.h
index 36d51862dd..87a652058c 100644
--- a/src/kernel/expr.h
+++ b/src/kernel/expr.h
@@ -217,22 +217,27 @@ class binder_info {
     /** \brief if m_inst_implicit is true, binder argument is an implicit argument, and should be
         inferred by class-instance resolution. */
     unsigned m_inst_implicit:1;
+    /** \brief Auxiliary internal attribute used to mark local constants represeting recursive functions
+        in recursive equations */
+    unsigned m_rec:1;
 public:
-    binder_info(bool implicit = false, bool contextual = true, bool strict_implicit = false, bool inst_implicit = false):
+    binder_info(bool implicit = false, bool contextual = true, bool strict_implicit = false, bool inst_implicit = false, bool rec = false):
         m_implicit(implicit), m_contextual(contextual), m_strict_implicit(strict_implicit),
-        m_inst_implicit(inst_implicit) {}
+        m_inst_implicit(inst_implicit), m_rec(rec) {}
     bool is_implicit() const { return m_implicit; }
     bool is_contextual() const { return m_contextual; }
     bool is_strict_implicit() const { return m_strict_implicit; }
     bool is_inst_implicit() const { return m_inst_implicit; }
+    bool is_rec() const { return m_rec; }
     unsigned hash() const;
-    binder_info update_contextual(bool f) const { return binder_info(m_implicit, f, m_strict_implicit, m_inst_implicit); }
+    binder_info update_contextual(bool f) const { return binder_info(m_implicit, f, m_strict_implicit, m_inst_implicit, m_rec); }
 };
 
 inline binder_info mk_implicit_binder_info()        { return binder_info(true); }
 inline binder_info mk_strict_implicit_binder_info() { return binder_info(false, true, true); }
 inline binder_info mk_inst_implicit_binder_info()   { return binder_info(false, true, false, true); }
 inline binder_info mk_contextual_info(bool f)       { return binder_info(false, f); }
+inline binder_info mk_rec_info(bool f)              { return binder_info(false, true, false, false, f); }
 
 inline bool is_explicit(binder_info const & bi) {
     return !bi.is_implicit() && !bi.is_strict_implicit() && !bi.is_inst_implicit();
diff --git a/src/library/blast/blast.cpp b/src/library/blast/blast.cpp
index d722dff5bf..21604919cf 100644
--- a/src/library/blast/blast.cpp
+++ b/src/library/blast/blast.cpp
@@ -451,9 +451,46 @@ class blastenv {
         g.get_hyps(hs);
         for (expr const & h : hs) {
             lean_assert(is_local(h));
-            expr new_type = normalize(to_blast_expr(mlocal_type(h)));
-            expr href     = s.mk_hypothesis(local_pp_name(h), new_type, h);
-            local2href.insert(mlocal_name(h), href);
+            if (!local_info(h).is_rec()) {
+                /*
+                  We do not add auxiliary locals used to compile recursive equations.
+                  The problem is that blast doesn't know when it is safe to use this kind of hypothesis.
+                  For example: suppose we are defining the following function using recursive equations and blast.
+
+                         lemma comm : ∀ a b : nat, a + b = b + a
+                         | a        0        := by simp
+                         | a        (succ n) := by simp
+
+                  Both goals will contain the (rec) hypothesis
+
+                         comm :  ∀ a b : nat, a + b = b + a
+
+                  If we the recursive equation is being compiled using structural recursion, then we can only apply
+                  'comm' to strucuturall smaller terms. If we are using well-founded recursion, then we need the well-founded relation.
+                  Blast does not have access to this information. We address this issue by simply ignoring this kind of
+                  auxiliary rec hypothesis.
+
+                  Of course, this workaround forces the user to provide a valid induction hypothesis.
+                  Example:
+
+                        lemma comm : ∀ a b : nat, a + b = b + a
+                        | a        0        := by simp
+                        | a        (succ n) :=
+                          assert a + n = n + a, from !comm,
+                          by simp
+
+                  In this simple example, we can simply ask blast to apply the recursor automatically for use.
+
+                        lemma comm : ∀ a b : nat, a + b = b + a :=
+                        by rec_simp
+
+                  However, this is not always possible. Sometimes, we will be defining a complex function using recursive equations.
+                  The definition may contain nested proofs that we may want to discharge using blast.
+                */
+                expr new_type = normalize(to_blast_expr(mlocal_type(h)));
+                expr href     = s.mk_hypothesis(local_pp_name(h), new_type, h);
+                local2href.insert(mlocal_name(h), href);
+            }
         }
         expr new_target = normalize(to_blast_expr(g.get_type()));
         s.set_target(new_target);
diff --git a/src/library/kernel_serializer.cpp b/src/library/kernel_serializer.cpp
index d51b045d36..d8b2601e21 100644
--- a/src/library/kernel_serializer.cpp
+++ b/src/library/kernel_serializer.cpp
@@ -118,6 +118,7 @@ static expr read_macro_definition(deserializer & d, unsigned num, expr const * a
 
 serializer & operator<<(serializer & s, binder_info const & i) {
     unsigned w =
+        (i.is_rec() ?            16 : 0) +
         (i.is_implicit() ?        8 : 0) +
         (i.is_contextual() ?      4 : 0) +
         (i.is_strict_implicit() ? 2 : 0) +
@@ -128,11 +129,12 @@ serializer & operator<<(serializer & s, binder_info const & i) {
 
 static binder_info read_binder_info(deserializer & d) {
     unsigned w = d.read_char();
-    bool imp   = (w & 8) != 0;
-    bool ctx   = (w & 4) != 0;
-    bool s_imp = (w & 2) != 0;
-    bool i_imp = (w & 1) != 0;
-    return binder_info(imp, ctx, s_imp, i_imp);
+    bool rec   = (w & 16) != 0;
+    bool imp   = (w & 8)  != 0;
+    bool ctx   = (w & 4)  != 0;
+    bool s_imp = (w & 2)  != 0;
+    bool i_imp = (w & 1)  != 0;
+    return binder_info(imp, ctx, s_imp, i_imp, rec);
 }
 
 static name * g_binder_name = nullptr;
diff --git a/tests/lean/run/blast_rec_eq.lean b/tests/lean/run/blast_rec_eq.lean
new file mode 100644
index 0000000000..35354ceb66
--- /dev/null
+++ b/tests/lean/run/blast_rec_eq.lean
@@ -0,0 +1,12 @@
+open nat
+
+lemma addz [simp] : ∀ a : nat, a + 0 = a := sorry
+lemma zadd [simp] : ∀ a : nat, 0 + a = a := sorry
+lemma adds [simp] : ∀ a b : nat, a + succ b = succ (a + b) := sorry
+lemma sadd [simp] : ∀ a b : nat, succ a + b = succ (a + b) := sorry
+
+definition comm : ∀ a b : nat, a + b = b + a
+| a        0        := by simp
+| a        (succ n) :=
+  assert a + n = n + a, from !comm,
+  by simp