diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp
index 21faaaf72..c715c8139 100644
--- a/src/frontends/lean/decl_cmds.cpp
+++ b/src/frontends/lean/decl_cmds.cpp
@@ -86,7 +86,7 @@ static void check_parameter_type(parser & p, name const & n, expr const & type,
     for_each(type, [&](expr const & e, unsigned) {
             if (is_local(e) && p.is_section_variable(e))
                 throw parser_error(sstream() << "invalid parameter declaration '" << n << "', it depends on " <<
-                                   "section variable '" << local_pp_name(e) << "'", pos);
+                                   "variable '" << local_pp_name(e) << "'", pos);
             return true;
         });
 }
@@ -96,12 +96,14 @@ static environment declare_var(parser & p, environment env,
                                variable_kind k, optional<binder_info> const & _bi, pos_info const & pos) {
     binder_info bi;
     if (_bi) bi = *_bi;
-    if (in_section_or_context(p.env())) {
-        lean_assert(k == variable_kind::Parameter || k == variable_kind::Variable);
-        if (k == variable_kind::Parameter)
+    if (k == variable_kind::Parameter || k == variable_kind::Variable) {
+        if (k == variable_kind::Parameter) {
+            check_in_section_or_context(p);
             check_parameter_type(p, n, type, pos);
+        }
         if (p.get_local(n))
-            throw parser_error(sstream() << "invalid declaration, section/context already contains '" << n << "'", pos);
+            throw parser_error(sstream() << "invalid parameter/variable declaration, '"
+                               << n << "' has already been declared", 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);
@@ -124,17 +126,15 @@ static environment declare_var(parser & p, environment env,
 }
 
 /** \brief If we are in a section, then add the new local levels to it. */
-static void update_section_local_levels(parser & p, level_param_names const & new_ls, bool is_variable) {
-    if (in_section_or_context(p.env())) {
-        for (auto const & l : new_ls)
-            p.add_local_level(l, mk_param_univ(l), is_variable);
-    }
+static void update_local_levels(parser & p, level_param_names const & new_ls, bool is_variable) {
+    for (auto const & l : new_ls)
+        p.add_local_level(l, mk_param_univ(l), is_variable);
 }
 
-optional<binder_info> parse_binder_info(parser & p) {
+optional<binder_info> parse_binder_info(parser & p, variable_kind k) {
     optional<binder_info> bi = p.parse_optional_binder_info();
-    if (bi)
-        check_in_section_or_context(p);
+    if (bi && k != variable_kind::Parameter && k != variable_kind::Variable)
+        parser_error("invalid binder annotation, it can only be used to declare variables/parameters", p.pos());
     return bi;
 }
 
@@ -144,8 +144,8 @@ static void check_variable_kind(parser & p, variable_kind k) {
             throw parser_error("invalid declaration, 'constant/axiom' cannot be used in sections/contexts",
                                p.pos());
     } else {
-        if (k == variable_kind::Parameter || k == variable_kind::Variable)
-            throw parser_error("invalid declaration, 'parameter/variable/hypothesis/conjecture' "
+        if (k == variable_kind::Parameter)
+            throw parser_error("invalid declaration, 'parameter/hypothesis/conjecture' "
                                "can only be used in sections/contexts", p.pos());
     }
 }
@@ -153,13 +153,13 @@ static void check_variable_kind(parser & p, variable_kind k) {
 environment variable_cmd_core(parser & p, variable_kind k) {
     check_variable_kind(p, k);
     auto pos = p.pos();
-    optional<binder_info> bi = parse_binder_info(p);
+    optional<binder_info> bi = parse_binder_info(p, k);
     name n = p.check_id_next("invalid declaration, identifier expected");
     buffer<name> ls_buffer;
-    if (p.curr_is_token(get_llevel_curly_tk()) && in_section_or_context(p.env()))
-        throw parser_error("invalid declaration, axioms/parameters occurring in sections cannot be universe polymorphic", p.pos());
+    if (p.curr_is_token(get_llevel_curly_tk()) && (k == variable_kind::Parameter || k == variable_kind::Variable))
+        throw parser_error("invalid declaration, only constants/axioms can be universe polymorphic", p.pos());
     optional<parser::local_scope> scope1;
-    if (!in_section_or_context(p.env()))
+    if (k == variable_kind::Constant || k == variable_kind::Axiom)
         scope1.emplace(p);
     parse_univ_params(p, ls_buffer);
     expr type;
@@ -175,7 +175,7 @@ environment variable_cmd_core(parser & p, variable_kind k) {
     }
     p.parse_close_binder_info(bi);
     level_param_names ls;
-    if (in_section_or_context(p.env())) {
+    if (ls_buffer.empty()) {
         ls = to_level_param_names(collect_univ_params(type));
     } else {
         update_univ_parameters(ls_buffer, collect_univ_params(type), p);
@@ -184,7 +184,8 @@ environment variable_cmd_core(parser & p, variable_kind k) {
     level_param_names new_ls;
     list<expr> ctx = p.locals_to_context();
     std::tie(type, new_ls) = p.elaborate_type(type, ctx);
-    update_section_local_levels(p, new_ls, k == variable_kind::Variable);
+    if (k == variable_kind::Variable || k == variable_kind::Parameter)
+        update_local_levels(p, new_ls, k == variable_kind::Variable);
     return declare_var(p, p.env(), n, append(ls, new_ls), type, k, bi, pos);
 }
 environment variable_cmd(parser & p) {
@@ -205,7 +206,7 @@ static environment variables_cmd_core(parser & p, variable_kind k) {
     auto pos = p.pos();
     environment env = p.env();
     while (true) {
-        optional<binder_info> bi = parse_binder_info(p);
+        optional<binder_info> bi = parse_binder_info(p, k);
         buffer<name> ids;
         while (!p.curr_is_token(get_colon_tk())) {
             name id = p.check_id_next("invalid parameters declaration, identifier expected");
@@ -213,7 +214,7 @@ static environment variables_cmd_core(parser & p, variable_kind k) {
         }
         p.next();
         optional<parser::local_scope> scope1;
-        if (!in_section_or_context(p.env()))
+        if (k == variable_kind::Constant || k == variable_kind::Axiom)
             scope1.emplace(p);
         expr type = p.parse_expr();
         p.parse_close_binder_info(bi);
@@ -225,7 +226,8 @@ static environment variables_cmd_core(parser & p, variable_kind k) {
             level_param_names new_ls;
             expr new_type;
             std::tie(new_type, new_ls) = p.elaborate_type(type, ctx);
-            update_section_local_levels(p, new_ls, k == variable_kind::Variable);
+            if (k == variable_kind::Variable || k == variable_kind::Parameter)
+                update_local_levels(p, new_ls, k == variable_kind::Variable);
             new_ls = append(ls, new_ls);
             env = declare_var(p, env, id, new_ls, new_type, k, bi, pos);
         }
@@ -245,7 +247,6 @@ static environment constants_cmd(parser & p) {
     return variables_cmd_core(p, variable_kind::Constant);
 }
 
-
 struct decl_modifiers {
     bool               m_is_instance;
     bool               m_is_coercion;
@@ -365,7 +366,7 @@ environment definition_cmd_core(parser & p, bool is_theorem, bool is_opaque, boo
         real_n     = ns + n;
     }
 
-    if (in_section_or_context(env)) {
+    if (p.has_locals()) {
         buffer<expr> section_ps;
         collect_section_locals(type, value, p, section_ps);
         type = Pi_as_is(section_ps, type, p);
@@ -515,7 +516,7 @@ environment include_cmd_core(parser & p, bool include) {
         name n = p.get_name_val();
         p.next();
         if (!p.get_local(n))
-            throw parser_error(sstream() << "invalid include/omit command, '" << n << "' is not a section parameter/variable", pos);
+            throw parser_error(sstream() << "invalid include/omit command, '" << n << "' is not a parameter/variable", pos);
         if (include) {
             if (p.is_include_variable(n))
                 throw parser_error(sstream() << "invalid include command, '" << n << "' has already been included", pos);
diff --git a/src/frontends/lean/inductive_cmd.cpp b/src/frontends/lean/inductive_cmd.cpp
index e056be54d..753b381a5 100644
--- a/src/frontends/lean/inductive_cmd.cpp
+++ b/src/frontends/lean/inductive_cmd.cpp
@@ -387,7 +387,7 @@ struct inductive_cmd_fn {
 
     /** \brief Include in m_levels any section level referenced by decls. */
     void include_section_levels(buffer<inductive_decl> const & decls) {
-        if (!in_section_or_context(m_env))
+        if (!m_p.has_locals())
             return;
         name_set all_lvl_params;
         for (auto const & d : decls) {
@@ -448,7 +448,7 @@ struct inductive_cmd_fn {
         The section parameters are stored in section_params
     */
     void abstract_section_locals(buffer<inductive_decl> & decls, buffer<expr> & section_params) {
-        if (!in_section_or_context(m_env))
+        if (!m_p.has_locals())
             return;
         expr_struct_set section_locals;
         collect_section_locals(decls, section_locals);
@@ -593,7 +593,7 @@ struct inductive_cmd_fn {
             id = name(name(full_id.get_prefix().get_string()), full_id.get_string());
         else
             id = name(full_id.get_string());
-        if (in_section_or_context(env)) {
+        if (!empty(section_levels) || !section_params.empty()) {
             expr r = mk_section_local_ref(full_id, section_levels, section_params);
             m_p.add_local_expr(id, r);
         }
diff --git a/src/frontends/lean/local_decls.h b/src/frontends/lean/local_decls.h
index 407370c2a..a996469b4 100644
--- a/src/frontends/lean/local_decls.h
+++ b/src/frontends/lean/local_decls.h
@@ -46,6 +46,7 @@ public:
         std::tie(m_map, m_counter, m_entries) = head(m_scopes);
         m_scopes  = tail(m_scopes);
     }
+    bool empty() const { return m_map.empty(); }
     struct mk_scope {
         local_decls & m_d;
         mk_scope(local_decls & d):m_d(d) { m_d.push(); }
diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h
index 5ea6ee6fb..0284d6670 100644
--- a/src/frontends/lean/parser.h
+++ b/src/frontends/lean/parser.h
@@ -331,6 +331,7 @@ public:
     expr parse_scoped_expr(buffer<expr> & ps, unsigned rbp = 0) { return parse_scoped_expr(ps.size(), ps.data(), rbp); }
 
     struct local_scope { parser & m_p; environment m_env; local_scope(parser & p); ~local_scope(); };
+    bool has_locals() const { return !m_local_decls.empty() || !m_local_level_decls.empty(); }
     void add_local_level(name const & n, level const & l, bool is_variable = false);
     void add_local_expr(name const & n, expr const & p, bool is_variable = false);
     void add_local(expr const & p) { return add_local_expr(local_pp_name(p), p); }
diff --git a/tests/lean/run/vars_anywhere.lean b/tests/lean/run/vars_anywhere.lean
new file mode 100644
index 000000000..fd48344ae
--- /dev/null
+++ b/tests/lean/run/vars_anywhere.lean
@@ -0,0 +1,11 @@
+variable {A : Type}
+
+definition id (a : A) := a
+
+check @id
+
+inductive list :=
+nil : list,
+cons : A → list → list
+
+check @list.cons
diff --git a/tests/lean/sec.lean.expected.out b/tests/lean/sec.lean.expected.out
index 5c89956cc..e49d1af06 100644
--- a/tests/lean/sec.lean.expected.out
+++ b/tests/lean/sec.lean.expected.out
@@ -1 +1 @@
-sec.lean:7:11: error: invalid declaration, section/context already contains 'A'
+sec.lean:7:11: error: invalid parameter/variable declaration, 'A' has already been declared
diff --git a/tests/lean/var.lean.expected.out b/tests/lean/var.lean.expected.out
index 6dc85136c..bca60353a 100644
--- a/tests/lean/var.lean.expected.out
+++ b/tests/lean/var.lean.expected.out
@@ -1 +1 @@
-var.lean:6:12: error: invalid parameter declaration 'a', it depends on section variable 'A'
+var.lean:6:12: error: invalid parameter declaration 'a', it depends on variable 'A'