diff --git a/library/init/lean/parser/parser.lean b/library/init/lean/parser/parser.lean
index 09a5fcbbb3..8266087bda 100644
--- a/library/init/lean/parser/parser.lean
+++ b/library/init/lean/parser/parser.lean
@@ -925,6 +925,20 @@ def checkWsBefore {k : ParserKind} (errorMsg : String) : Parser k :=
 { info := epsilonInfo,
   fn   := fun _ => checkWsBeforeFn errorMsg }
 
+def checkTailNoWs (prev : Syntax) : Bool :=
+match prev.getTailInfo with
+| some info => info.trailing.stopPos == info.trailing.startPos
+| none      => false
+
+def checkNoWsBeforeFn (errorMsg : String) : BasicParserFn :=
+fun c s =>
+  let prev := s.stxStack.back;
+  if checkTailNoWs prev then s else s.mkError errorMsg
+
+def checkNoWsBefore {k : ParserKind} (errorMsg : String) : Parser k :=
+{ info := epsilonInfo,
+  fn   := fun _ => checkNoWsBeforeFn errorMsg }
+
 def insertNoWsToken (sym : String) (lbpNoWs : Option Nat) (tks : TokenTable) : ExceptT String Id TokenTable :=
 if sym == "" then throw "invalid empty symbol"
 else match tks.find sym, lbpNoWs with
@@ -939,11 +953,6 @@ def symbolNoWsInfo (sym : String) (lbpNoWs : Option Nat) : ParserInfo :=
 { updateTokens := insertNoWsToken sym lbpNoWs,
   firstTokens  := FirstTokens.tokens [ { val := sym, lbpNoWs := lbpNoWs } ] }
 
-def checkTailNoWs (left : Syntax) : Bool :=
-match left.getTailInfo with
-| some info => info.trailing.stopPos == info.trailing.startPos
-| none      => false
-
 @[inline] def symbolNoWsFnAux (sym : String) (errorMsg : String) : ParserFn trailing :=
 fun left c s =>
   if checkTailNoWs left then
diff --git a/library/init/lean/parser/term.lean b/library/init/lean/parser/term.lean
index f74b65279a..843f7e75cd 100644
--- a/library/init/lean/parser/term.lean
+++ b/library/init/lean/parser/term.lean
@@ -41,7 +41,9 @@ def infixL (sym : String) (lbp : Nat) : TrailingParser :=
 pushLeading >> symbol sym lbp >> termParser lbp
 
 /- Builting parsers -/
-@[builtinTermParser] def id := parser! ident >> optional (".{" >> sepBy1 levelParser ", " >> "}")
+def explicitUniv   := parser! ".{" >> sepBy1 levelParser ", " >> "}"
+def namedPattern := parser! checkNoWsBefore "no space before '@'" >> "@" >> termParser appPrec
+@[builtinTermParser] def id := parser! ident >> optional (explicitUniv <|> namedPattern)
 @[builtinTermParser] def num : Parser := numLit
 @[builtinTermParser] def str : Parser := strLit
 @[builtinTermParser] def char : Parser := charLit