diff --git a/library/init/lean/parser/term.lean b/library/init/lean/parser/term.lean
index c052bafcf2..49674ac597 100644
--- a/library/init/lean/parser/term.lean
+++ b/library/init/lean/parser/term.lean
@@ -21,7 +21,7 @@ def termParser {k : ParserKind} (rbp : Nat := 0) : Parser k :=
 
 namespace Term
 
-@[builtinTermParser] def ident := parser! ident >> optional (".{" >> many1 levelParser >> "}")
+@[builtinTermParser] def ident := parser! ident >> optional (".{" >> sepBy1 levelParser ", " >> "}")
 @[builtinTermParser] def num : Parser := numLit
 @[builtinTermParser] def str : Parser := strLit
 @[builtinTermParser] def type := parser! symbol "Type" maxPrec
diff --git a/tests/playground/termparsertest1.lean b/tests/playground/termparsertest1.lean
index 92f5f7b198..447e40d037 100644
--- a/tests/playground/termparsertest1.lean
+++ b/tests/playground/termparsertest1.lean
@@ -11,10 +11,11 @@ IO.println stx
 
 def main (xs : List String) : IO Unit :=
 do
-testParser "x.{u v+1}";
+testParser "x.{u, v+1}";
+testParser "x.{u}";
 testParser "x";
 testParser "x.{max u v}";
-testParser "x.{(max u v) 0}";
+testParser "x.{max u v, 0}";
 testParser "f 0 1";
 testParser "f.{u+1} \"foo\" x";
 testParser "(f x, 0, 1)";