From a1fc82433611e41d2de550752a8b0adecb864e04 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 17 Jul 2020 10:12:43 -0700
Subject: [PATCH] fix: field syntax

---
 src/Lean/Parser/Command.lean | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean
index 17ca8c271e..966c386db4 100644
--- a/src/Lean/Parser/Command.lean
+++ b/src/Lean/Parser/Command.lean
@@ -57,9 +57,9 @@ def inferMod         := parser! try ("{" >> "}")
 def ctor             := parser! " | " >> declModifiers >> ident >> optional inferMod >> optDeclSig
 def «inductive»      := parser! "inductive " >> declId >> optDeclSig >> many ctor
 def classInductive   := parser! try ("class " >> "inductive ") >> declId >> optDeclSig >> many ctor
-def structExplicitBinder := parser! try (declModifiers >> "(") >> many ident >> optional inferMod >> declSig >> optional Term.binderDefault >> ")"
-def structImplicitBinder := parser! try (declModifiers >> "{") >> many ident >> optional inferMod >> declSig >> "}"
-def structInstBinder     := parser! try (declModifiers >> "[") >> many ident >> optional inferMod >> declSig >> "]"
+def structExplicitBinder := parser! try (declModifiers >> "(") >> many1 ident >> optional inferMod >> declSig >> optional Term.binderDefault >> ")"
+def structImplicitBinder := parser! try (declModifiers >> "{") >> many1 ident >> optional inferMod >> declSig >> "}"
+def structInstBinder     := parser! try (declModifiers >> "[") >> many1 ident >> optional inferMod >> declSig >> "]"
 def structFields         := parser! many (structExplicitBinder <|> structImplicitBinder <|> structInstBinder)
 def structCtor           := parser! try (declModifiers >> ident >> optional inferMod >> " :: ")
 def structureTk          := parser! "structure "