From 5f1d827b2629e642e7f1c9d9969544111d511488 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 25 Mar 2015 13:42:07 -0700
Subject: [PATCH] fix(frontends/lean/decl_cmds): assertion violation

closes #506
---
 src/frontends/lean/decl_cmds.cpp       | 2 +-
 tests/lean/match_bug.lean              | 3 +++
 tests/lean/match_bug.lean.expected.out | 1 +
 3 files changed, 5 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/match_bug.lean
 create mode 100644 tests/lean/match_bug.lean.expected.out

diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp
index 901be56a2..b1128e936 100644
--- a/src/frontends/lean/decl_cmds.cpp
+++ b/src/frontends/lean/decl_cmds.cpp
@@ -510,7 +510,7 @@ static void validate_equation_lhs(parser const & p, expr const & lhs, buffer<exp
                     std::any_of(locals.begin(), locals.end(), [&](expr const & local) {
                             return mlocal_name(e) == mlocal_name(local);
                         })) {
-                    throw parser_error(sstream() << "invalid occurrence of variable '" << mlocal_name(lhs) <<
+                    throw parser_error(sstream() << "invalid occurrence of variable '" << mlocal_name(e) <<
                                        "' in the left-hand-side of recursive equation", p.pos_of(lhs));
                 }
                 return has_local(e);
diff --git a/tests/lean/match_bug.lean b/tests/lean/match_bug.lean
new file mode 100644
index 000000000..4d9b73be1
--- /dev/null
+++ b/tests/lean/match_bug.lean
@@ -0,0 +1,3 @@
+definition foo : nat -> nat := fun x,
+match x with
+| bar -> bar
diff --git a/tests/lean/match_bug.lean.expected.out b/tests/lean/match_bug.lean.expected.out
new file mode 100644
index 000000000..5d7bfa785
--- /dev/null
+++ b/tests/lean/match_bug.lean.expected.out
@@ -0,0 +1 @@
+match_bug.lean:3:6: error: invalid occurrence of variable 'bar' in the left-hand-side of recursive equation