From c01da783ca9bcbc5cc12fdbdc6a672f0f08ec743 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 20 May 2020 15:49:40 -0700
Subject: [PATCH] fix: `{ ... : <expected-type> }` syntax in the old frontend

---
 src/frontends/lean/brackets.cpp | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/src/frontends/lean/brackets.cpp b/src/frontends/lean/brackets.cpp
index b2cf3001e7..7dee425acb 100644
--- a/src/frontends/lean/brackets.cpp
+++ b/src/frontends/lean/brackets.cpp
@@ -82,6 +82,8 @@ static expr parse_structure_instance_core(parser & p, optional<expr> const & src
             p.next();
             catchall = true;
             break;
+        } else if (p.curr_is_token(get_colon_tk())) {
+            break;
         } else if (!read_source) {
             fns.push_back(p.check_id_next("invalid structure instance, identifier expected"));
             p.check_token_next(get_assign_tk(), "invalid structure instance, ':=' expected");
@@ -176,6 +178,8 @@ expr parse_curly_bracket(parser & p, unsigned, expr const *, pos_info const & po
         return p.save_pos(mk_structure_instance(), pos);
     } else if (p.curr_is_token(get_dotdot_tk())) {
         return parse_structure_instance_core(p);
+    } else if (p.curr_is_token(get_colon_tk())) {
+        return parse_structure_instance_core(p);
     } else {
         e = p.parse_expr();
     }