diff --git a/src/Lean/Parser/Basic.lean b/src/Lean/Parser/Basic.lean
index 9342d5a938c7..56ad17794c0b 100644
--- a/src/Lean/Parser/Basic.lean
+++ b/src/Lean/Parser/Basic.lean
@@ -1295,7 +1295,20 @@ def nameLitNoAntiquot : Parser := {
   info := mkAtomicInfo "name"
 }
 
-def identFn : ParserFn := expectTokenFn identKind "identifier"
+def identFn : ParserFn := fun c s =>
+  if c.forbiddenTks.isEmpty then
+    expectTokenFn identKind "identifier" c s
+  else
+    -- A forbidden token used as an identifier (e.g. a non-reserved clause keyword like
+    -- `invariant`) stops the enclosing term, mirroring `mkTokenAndFixPos`.
+    let iniSz  := s.stackSize
+    let iniPos := s.pos
+    let s := expectTokenFn identKind "identifier" c s
+    if s.hasError then s
+    else match s.stxStack.back with
+      | .ident _ rawVal _ _ =>
+        if c.forbiddenTks.contains rawVal.toString then s.mkErrorAt "forbidden token" iniPos iniSz else s
+      | _ => s
 
 def identNoAntiquot : Parser := {
   fn   := identFn
diff --git a/tests/elab/forbiddenIdentifiers.lean b/tests/elab/forbiddenIdentifiers.lean
new file mode 100644
index 000000000000..34684fd91043
--- /dev/null
+++ b/tests/elab/forbiddenIdentifiers.lean
@@ -0,0 +1,30 @@
+import Lean
+/-!
+`withForbidden` stops a term at a non-reserved word used as a bare identifier, while the word
+stays usable as an identifier (escaped, projected, or a plain declaration name).
+-/
+open Lean Elab Command Parser
+
+namespace ForbiddenIdentTest
+
+-- `#collect e sep e'` parses `e` with the non-reserved word `sep` forbidden, so a bare `sep`
+-- ends `e` without `sep` being a reserved keyword.
+@[command_parser]
+def collectCmd : Parser := leading_parser
+  "#collect " >> withForbidden "sep" termParser >> nonReservedSymbol "sep" >> ppSpace >> termParser
+
+@[command_elab collectCmd]
+def elabCollect : CommandElab := fun _ => pure ()
+
+-- A bare `sep` ends the first term (requires the forbidding; else `a sep` is an application).
+#collect a sep b
+-- A multi-token first term still stops at the bare `sep`.
+#collect f a sep b
+-- Escaped `«sep»` is not forbidden: it is consumed as the first term.
+#collect «sep» sep b
+-- A projection `.sep` (rawIdent path) is not forbidden.
+#collect (id x).sep sep b
+-- The word remains usable as an ordinary identifier.
+def sep : Nat := 0
+
+end ForbiddenIdentTest