diff --git a/src/library/scoped_ext.cpp b/src/library/scoped_ext.cpp
index 30a532c28f..fc787182a5 100644
--- a/src/library/scoped_ext.cpp
+++ b/src/library/scoped_ext.cpp
@@ -99,7 +99,9 @@ static std::string g_new_namespace_key("nspace");
 environment push_scope(environment const & env, io_state const & ios, scope_kind k, name const & n) {
     if (k == scope_kind::Namespace && in_section_or_context(env))
         throw exception("invalid namespace declaration, a namespace cannot be declared inside a section or context");
-    name new_n = get_namespace(env) + n;
+    name new_n = get_namespace(env);
+    if (k == scope_kind::Namespace)
+        new_n = new_n + n;
     scope_mng_ext ext = get_extension(env);
     bool save_ns = false;
     if (!ext.m_namespace_set.contains(new_n)) {
diff --git a/tests/lean/run/sec_bug.lean b/tests/lean/run/sec_bug.lean
new file mode 100644
index 0000000000..c7500b97dd
--- /dev/null
+++ b/tests/lean/run/sec_bug.lean
@@ -0,0 +1,9 @@
+import logic
+
+namespace foo
+section bla
+  definition tst := true
+end bla
+end foo
+
+check foo.tst