diff --git a/src/frontends/lean/decl_util.cpp b/src/frontends/lean/decl_util.cpp
index 6ab910e826..f3e505c4e6 100644
--- a/src/frontends/lean/decl_util.cpp
+++ b/src/frontends/lean/decl_util.cpp
@@ -273,8 +273,6 @@ void collect_implicit_locals(parser & p, buffer<name> & lp_names, buffer<expr> &
     for (expr const & e : all_exprs) {
         collect_locals_ignoring_tactics(e, locals);
         lp_found = collect_univ_params_ignoring_tactics(e, lp_found);
-        if (is_local(e))
-            given_params.insert(mlocal_name(e));
     }
     collect_annonymous_inst_implicit(p, locals);
     sort_locals(locals.get_collected(), p, params);
diff --git a/tests/lean/run/include_bug.lean b/tests/lean/run/include_bug.lean
new file mode 100644
index 0000000000..c6cdaaffd5
--- /dev/null
+++ b/tests/lean/run/include_bug.lean
@@ -0,0 +1,5 @@
+variables x y : nat
+variable xy : x = y
+
+include xy
+lemma xyeq : x = y := xy