diff --git a/src/frontends/lean/brackets.cpp b/src/frontends/lean/brackets.cpp
index d9dd048cbc..74096a61ad 100644
--- a/src/frontends/lean/brackets.cpp
+++ b/src/frontends/lean/brackets.cpp
@@ -36,7 +36,7 @@ static expr mk_singleton(parser & p, pos_info const & pos, expr const & e) {
 
 /* Parse rest of the insertable '{' expr ... */
 static expr parse_insertable(parser & p, pos_info const & pos, expr const & e) {
-    lean_assert(p.curr_is_token(get_comma_tk()));
+    lean_assert(p.curr_is_token(get_comma_tk()) || p.curr_is_token(get_rcurly_tk()));
     expr r = mk_singleton(p, pos, e);
     while (p.curr_is_token(get_comma_tk())) {
         auto ins_pos = p.pos();
diff --git a/src/frontends/lean/structure_instance.cpp b/src/frontends/lean/structure_instance.cpp
index ca4dd7ed8a..5aac95b09f 100644
--- a/src/frontends/lean/structure_instance.cpp
+++ b/src/frontends/lean/structure_instance.cpp
@@ -45,7 +45,7 @@ public:
 };
 
 static expr mk_structure_instance_core(name const & s, list<name> const & fs, unsigned num, expr const * args) {
-    lean_assert(num == length(fs) && num == length(fs) + 1);
+    lean_assert(num == length(fs) || num == length(fs) + 1);
     macro_definition def(new structure_instance_macro_cell(s, fs));
     return mk_macro(def, num, args);
 }