diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index 4f13e3b78c..e53c72fbf4 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -1813,6 +1813,7 @@ expr elaborator::visit_structure_instance(expr const & e, optional<expr> const &
     get_structure_instance_info(e, S_name, src, fnames, fvalues);
     lean_assert(fnames.size() == fvalues.size());
     name src_S_name;
+    unsigned src_S_nparams = 0;
     if (src) {
         src = visit(*src, none_expr());
         synthesize_type_class_instances();
@@ -1826,7 +1827,8 @@ expr elaborator::visit_structure_instance(expr const & e, optional<expr> const &
                                        line() + format("which has type") +
                                        pp_indent(pp_fn, type));
         }
-        src_S_name = const_name(src_S);
+        src_S_name    = const_name(src_S);
+        src_S_nparams = *inductive::get_num_params(m_env, src_S_name);
     }
     if (S_name.is_anonymous()) {
         if (expected_type) {
@@ -1879,6 +1881,9 @@ expr elaborator::visit_structure_instance(expr const & e, optional<expr> const &
                     if (src) {
                         name new_fname = src_S_name + S_fname;
                         expr f = copy_tag(e, mk_constant(new_fname));
+                        f = copy_tag(e, mk_explicit(f));
+                        for (unsigned i = 0; i < src_S_nparams; i++)
+                            f = copy_tag(e, mk_app(f, copy_tag(e, mk_expr_placeholder())));
                         f = copy_tag(e, mk_app(f, *src));
                         try {
                             f = visit(f, none_expr());
diff --git a/tests/lean/run/with_update_class.lean b/tests/lean/run/with_update_class.lean
new file mode 100644
index 0000000000..749ea65f09
--- /dev/null
+++ b/tests/lean/run/with_update_class.lean
@@ -0,0 +1,10 @@
+universe variables u
+
+class foo (A : Type u) :=
+(x : A)
+
+class bla (A : Type u) extends foo A :=
+(y : nat)
+
+def ex {A : Type u} [s : foo A] : bla A :=
+{ s with y := 0 }