diff --git a/doc/changes.md b/doc/changes.md
index 25f7d55a4a..d6744ec191 100644
--- a/doc/changes.md
+++ b/doc/changes.md
@@ -3,6 +3,8 @@ master branch (aka work in progress branch)
 
 *Features*
 
+- Implemented [RFC #1820](https://github.com/leanprover/lean/issues/1820)
+
 *Changes*
 
 *API name changes*
diff --git a/src/frontends/lean/brackets.cpp b/src/frontends/lean/brackets.cpp
index 61b40d5e0e..9f21af1ba4 100644
--- a/src/frontends/lean/brackets.cpp
+++ b/src/frontends/lean/brackets.cpp
@@ -113,8 +113,16 @@ static expr parse_structure_instance(parser & p, name const & fname) {
 
 /* Parse rest of the structure instance update '{' expr 'with' ... */
 static expr parse_structure_instance_update(parser & p, expr const & e) {
-    name fname = p.check_id_next("invalid structure update, identifier expected");
-    return parse_structure_instance_core(p, some_expr(e), name(), fname);
+    if (p.curr_is_token(get_rcurly_tk())) {
+        // '{' expr 'with' '}'
+        p.next();
+        buffer<name> fns;
+        buffer<expr> fvs;
+        return mk_structure_instance(e, fns, fvs);
+    } else {
+        name fname = p.check_id_next("invalid structure update, identifier expected");
+        return parse_structure_instance_core(p, some_expr(e), name(), fname);
+    }
 }
 
 static name * g_emptyc_or_emptys = nullptr;
diff --git a/tests/lean/run/1820.lean b/tests/lean/run/1820.lean
new file mode 100644
index 0000000000..d4860d6701
--- /dev/null
+++ b/tests/lean/run/1820.lean
@@ -0,0 +1,12 @@
+def f (p : nat × nat) : nat × nat := {p with}
+
+structure P (A : Type) extends prod A A :=
+(third : A)
+
+def g (s : P nat) : nat × nat := {s with}
+
+example : g (P.mk (1, 2) 3) = (1, 2) :=
+rfl
+
+example : g ⟨⟨1, 2⟩, 3⟩ = (1, 2) :=
+rfl