From 6fa6554b4de16be7495f3d4098200fc6bb4c0b92 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 21 Jun 2016 16:30:26 -0700
Subject: [PATCH] fix(library/tactic/intro_tactic): fix 'intron' tactic

---
 src/library/tactic/intro_tactic.cpp | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/src/library/tactic/intro_tactic.cpp b/src/library/tactic/intro_tactic.cpp
index dfbc0c3202..0f16e1e191 100644
--- a/src/library/tactic/intro_tactic.cpp
+++ b/src/library/tactic/intro_tactic.cpp
@@ -53,7 +53,12 @@ optional<tactic_state> intron(unsigned n, tactic_state const & s, buffer<name> &
         optional<local_decl> d = lctx.get_local_decl(new_Hs[i]);
         expr type = d->get_type();
         type      = abstract_locals(type, i, new_Hs.data());
-        new_val   = mk_lambda(d->get_pp_name(), type, new_val, d->get_info());
+        if (auto letval = d->get_value()) {
+            letval    = abstract_locals(*letval, i, new_Hs.data());
+            new_val   = mk_let(d->get_pp_name(), type, *letval, new_val);
+        } else {
+            new_val   = mk_lambda(d->get_pp_name(), type, new_val, d->get_info());
+        }
     }
     lean_assert(!mctx.is_assigned(new_M));
     mctx.assign(head(s.goals()), new_val);