From df3100d2cd4b2b36344417316b1c9d47139ae93c Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 12 Sep 2015 17:17:13 -0700
Subject: [PATCH] fix(library/local_context): bug in abstract_locals procedure

---
 src/kernel/abstract.cpp           |  2 +-
 src/library/local_context.cpp     |  2 +-
 tests/lean/run/local_ctx_bug.lean | 25 +++++++++++++++++++++++++
 3 files changed, 27 insertions(+), 2 deletions(-)
 create mode 100644 tests/lean/run/local_ctx_bug.lean

diff --git a/src/kernel/abstract.cpp b/src/kernel/abstract.cpp
index 8d236f30ca..8bb555ee54 100644
--- a/src/kernel/abstract.cpp
+++ b/src/kernel/abstract.cpp
@@ -43,7 +43,7 @@ expr abstract_locals(expr const & e, unsigned n, expr const * subst) {
                     if (mlocal_name(subst[i]) == mlocal_name(m))
                         return some_expr(mk_var(offset + n - i - 1, m.get_tag()));
                 }
-                return some_expr(m);
+                return none_expr();
             }
             return none_expr();
         });
diff --git a/src/library/local_context.cpp b/src/library/local_context.cpp
index 265ec4f8b5..369c2f765d 100644
--- a/src/library/local_context.cpp
+++ b/src/library/local_context.cpp
@@ -31,7 +31,7 @@ expr local_context::abstract_locals(expr const & e, list<expr> const & locals) {
                         return some_expr(copy_tag(m, mk_var(offset + i)));
                     i++;
                 }
-                return some_expr(m);
+                return none_expr();
             }
             return none_expr();
         });
diff --git a/tests/lean/run/local_ctx_bug.lean b/tests/lean/run/local_ctx_bug.lean
new file mode 100644
index 0000000000..5a78c928cd
--- /dev/null
+++ b/tests/lean/run/local_ctx_bug.lean
@@ -0,0 +1,25 @@
+import data.finset data.finset.card data.finset.equiv
+open nat nat.finset decidable
+
+namespace finset
+variable {A : Type}
+open finset (to_nat)
+open finset (of_nat)
+
+private lemma of_nat_eq_insert : ∀ {n s : nat}, n ∉ of_nat s → of_nat (2^n + s) = insert n (of_nat s)
+| 0        s h := sorry
+| (succ n) s h :=
+  have n ∉ of_nat s,                     from sorry,
+  assert of_nat s = insert n (of_nat s), from sorry,
+  finset.ext (λ x,
+  have gen : ∀ m, m ∈ of_nat (2^(succ n) + s) ↔ m ∈ insert (succ n) (of_nat s)
+  | zero     :=
+    assert aux₁ : odd (2^(succ n) + s) ↔ odd s, from sorry,
+    calc
+      0 ∈ of_nat (2^(succ n) + s) ↔ odd (2^(succ n) + s)           : sorry
+                             ...  ↔ odd s                          : aux₁
+                             ...  ↔ 0 ∈ insert (succ n) (of_nat s) : sorry
+  | (succ m) := sorry,
+  gen x)
+
+end finset