diff --git a/src/frontends/lean/structure_cmd.cpp b/src/frontends/lean/structure_cmd.cpp
index b78961cbd8..c340ffd192 100644
--- a/src/frontends/lean/structure_cmd.cpp
+++ b/src/frontends/lean/structure_cmd.cpp
@@ -466,7 +466,7 @@ struct structure_cmd_fn {
         return ::lean::mk_field_default_value(m_env, full_field_name, [&](name const & fname) {
                 for (field_decl const & d : m_fields) {
                     if (local_pp_name(d.first) == fname)
-                        return some_expr(d.first);
+                        return some_expr(mk_explicit(d.first));
                 }
                 return none_expr();
             });
diff --git a/tests/lean/run/struct_bug3.lean b/tests/lean/run/struct_bug3.lean
new file mode 100644
index 0000000000..75bcb6f6db
--- /dev/null
+++ b/tests/lean/run/struct_bug3.lean
@@ -0,0 +1,5 @@
+structure foo :=
+(f : Π {α : Type}, α)
+(g : Π {α : Type}, α := @f)
+
+structure bar extends foo