From 613281d622c553d8d40b828b35ecb83a373db056 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 6 May 2015 10:01:24 -0700
Subject: [PATCH] fix(frontends/lean/builtin_exprs): bug in new 'obtain'
 expression

---
 src/frontends/lean/builtin_exprs.cpp | 10 +++++++---
 tests/lean/run/new_obtain3.lean      | 15 +++++++++++++++
 2 files changed, 22 insertions(+), 3 deletions(-)
 create mode 100644 tests/lean/run/new_obtain3.lean

diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp
index dfe8ecabf..5b5202d7a 100644
--- a/src/frontends/lean/builtin_exprs.cpp
+++ b/src/frontends/lean/builtin_exprs.cpp
@@ -457,6 +457,7 @@ static expr parse_show(parser & p, unsigned, expr const *, pos_info const & pos)
 
 static obtain_struct parse_obtain_decls (parser & p, buffer<expr> & ps) {
     buffer<obtain_struct> children;
+    parser::local_scope scope(p);
     while (!p.curr_is_token(get_comma_tk()) && !p.curr_is_token(get_rbracket_tk())) {
         if (p.curr_is_token(get_lbracket_tk())) {
             p.next();
@@ -464,11 +465,14 @@ static obtain_struct parse_obtain_decls (parser & p, buffer<expr> & ps) {
             children.push_back(s);
             p.check_token_next(get_rbracket_tk(), "invalid 'obtain' expression, ']' expected");
         } else {
-            unsigned old_sz = ps.size();
             unsigned rbp = 0;
-            p.parse_simple_binders(ps, rbp);
-            for (unsigned i = old_sz; i < ps.size(); i++)
+            buffer<expr> new_ps;
+            p.parse_simple_binders(new_ps, rbp);
+            for (expr const & l : new_ps) {
+                ps.push_back(l);
+                p.add_local(l);
                 children.push_back(obtain_struct());
+            }
         }
     }
     if (children.empty())
diff --git a/tests/lean/run/new_obtain3.lean b/tests/lean/run/new_obtain3.lean
new file mode 100644
index 000000000..a75dfda50
--- /dev/null
+++ b/tests/lean/run/new_obtain3.lean
@@ -0,0 +1,15 @@
+import data.set
+open set function eq.ops
+
+variables {X Y Z : Type}
+
+lemma image_compose (f : Y → X) (g : X → Y) (a : set X) : (f ∘ g) '[a] = f '[g '[a]] :=
+setext (take z,
+  iff.intro
+    (assume Hz : z ∈ (f ∘ g) '[a],
+      obtain x (Hx₁ : x ∈ a) (Hx₂ : f (g x) = z), from Hz,
+      have Hgx : g x ∈ g '[a], from in_image Hx₁ rfl,
+      show z ∈ f '[g '[a]], from in_image Hgx Hx₂)
+    (assume Hz : z ∈ f '[g '[a]],
+      obtain y [x (Hz₁ : x ∈ a) (Hz₂ : g x = y)] (Hy₂ : f y = z), from Hz,
+      show z ∈ (f ∘ g) '[a], from in_image Hz₁ (Hz₂⁻¹ ▸ Hy₂)))