diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp
index 3b5715b55..e03622b1c 100644
--- a/src/frontends/lean/decl_cmds.cpp
+++ b/src/frontends/lean/decl_cmds.cpp
@@ -85,6 +85,8 @@ static environment declare_var(parser & p, environment env,
         lean_assert(k == variable_kind::Parameter || k == variable_kind::Variable);
         if (k == variable_kind::Parameter)
             check_parameter_type(p, n, type, pos);
+        if (p.get_local(n))
+            throw parser_error(sstream() << "invalid declaration, section/context already contains '" << n << "'", pos);
         name u = p.mk_fresh_name();
         expr l = p.save_pos(mk_local(u, n, type, bi), pos);
         p.add_local_expr(n, l, k == variable_kind::Variable);
diff --git a/tests/lean/sec.lean b/tests/lean/sec.lean
new file mode 100644
index 000000000..ec306d76e
--- /dev/null
+++ b/tests/lean/sec.lean
@@ -0,0 +1,11 @@
+import data.prod
+open prod
+
+section
+  variable A : Type
+  variable a : A
+  variable A : Type
+  variable b : A
+
+  definition foo := a
+end
diff --git a/tests/lean/sec.lean.expected.out b/tests/lean/sec.lean.expected.out
new file mode 100644
index 000000000..5c89956cc
--- /dev/null
+++ b/tests/lean/sec.lean.expected.out
@@ -0,0 +1 @@
+sec.lean:7:11: error: invalid declaration, section/context already contains 'A'