diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp
index 73619ae8c..fd7ab27f9 100644
--- a/src/frontends/lean/builtin_cmds.cpp
+++ b/src/frontends/lean/builtin_cmds.cpp
@@ -602,6 +602,8 @@ static void parse_metaclasses(parser & p, buffer<name> & r) {
         while (p.curr_is_token(get_lbracket_tk())) {
             name m = parse_metaclass(p);
             tmp.erase_elem(m);
+            if (m == get_declarations_tk())
+                tmp.erase_elem(get_decls_tk());
         }
         r.append(tmp);
     } else {
diff --git a/tests/lean/run/568.lean b/tests/lean/run/568.lean
new file mode 100644
index 000000000..d79773020
--- /dev/null
+++ b/tests/lean/run/568.lean
@@ -0,0 +1,15 @@
+namespace f1
+  definition flip := 20
+end f1
+
+namespace f2
+  definition flip := 10
+end f2
+
+namespace f3
+  export [declarations] f1
+  export -[declarations] f2
+end f3
+
+export [declarations] f1
+export -[declarations] f2