diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean
index 1e3b9413a0..f78c902762 100644
--- a/src/Lean/Parser/Term.lean
+++ b/src/Lean/Parser/Term.lean
@@ -260,7 +260,7 @@ def argument       :=
 -- argument precedence is `arg` (i.e. does not accept `lead` precedence)
 @[builtinTermParser] def app      := trailing_parser:leadPrec:maxPrec many1 argument
 
-@[builtinTermParser] def proj     := trailing_parser checkNoWsBefore >> "." >> checkNoWsBefore >> (fieldIdx <|> ident)
+@[builtinTermParser] def proj     := trailing_parser checkNoWsBefore >> "." >> checkNoWsBefore >> (fieldIdx <|> rawIdent)
 @[builtinTermParser] def completion := trailing_parser checkNoWsBefore >> "."
 @[builtinTermParser] def arrayRef := trailing_parser checkNoWsBefore >> "[" >> termParser >>"]"
 @[builtinTermParser] def arrow    := trailing_parser checkPrec 25 >> unicodeSymbol " → " " -> " >> termParser 25
@@ -272,7 +272,7 @@ def isIdent (stx : Syntax) : Bool :=
 @[builtinTermParser] def explicitUniv : TrailingParser := trailing_parser checkStackTop isIdent "expected preceding identifier" >> checkNoWsBefore "no space before '.{'" >> ".{" >> sepBy1 levelParser ", " >> "}"
 @[builtinTermParser] def namedPattern : TrailingParser := trailing_parser checkStackTop isIdent "expected preceding identifier" >> checkNoWsBefore "no space before '@'" >> "@" >> optional (atomic (ident >> ":")) >> termParser maxPrec
 
-@[builtinTermParser] def pipeProj   := trailing_parser:minPrec " |>." >> checkNoWsBefore >> (fieldIdx <|> ident) >> many argument
+@[builtinTermParser] def pipeProj   := trailing_parser:minPrec " |>." >> checkNoWsBefore >> (fieldIdx <|> rawIdent) >> many argument
 @[builtinTermParser] def pipeCompletion := trailing_parser:minPrec " |>."
 
 @[builtinTermParser] def subst := trailing_parser:75 " ▸ " >> sepBy1 (termParser 75) " ▸ "
@@ -299,7 +299,7 @@ def macroLastArg   := macroDollarArg <|> macroArg
 
 @[builtinTermParser] def dynamicQuot := leading_parser "`(" >> ident >> "|" >> incQuotDepth (parserOfStack 1) >> ")"
 
-@[builtinTermParser] def dotIdent := leading_parser "." >> checkNoWsBefore >> ident
+@[builtinTermParser] def dotIdent := leading_parser "." >> checkNoWsBefore >> rawIdent
 
 end Term
 
diff --git a/tests/lean/run/constProp.lean b/tests/lean/run/constProp.lean
index 679bb82627..69accd9048 100644
--- a/tests/lean/run/constProp.lean
+++ b/tests/lean/run/constProp.lean
@@ -226,8 +226,8 @@ inductive Bigstep : State → Stmt → State → Prop where
   | seq        : (σ₁, s₁) ⇓ σ₂ → (σ₂, s₂) ⇓ σ₃ → (σ₁, s₁ ;; s₂) ⇓ σ₃
   | ifTrue     : evalTrue c σ₁ → (σ₁, t) ⇓ σ₂ → (σ₁, .ite c t e) ⇓ σ₂
   | ifFalse    : evalFalse c σ₁ → (σ₁, e) ⇓ σ₂ → (σ₁, .ite c t e) ⇓ σ₂
-  | whileTrue  : evalTrue c σ₁ → (σ₁, b) ⇓ σ₂ → (σ₂, .«while» c b) ⇓ σ₃ → (σ₁, .«while» c b) ⇓ σ₃
-  | whileFalse : evalFalse c σ → (σ, .«while» c b) ⇓ σ
+  | whileTrue  : evalTrue c σ₁ → (σ₁, b) ⇓ σ₂ → (σ₂, .while c b) ⇓ σ₃ → (σ₁, .while c b) ⇓ σ₃
+  | whileFalse : evalFalse c σ → (σ, .while c b) ⇓ σ
 
 end
 
@@ -268,7 +268,7 @@ def evalExpr (e : Expr) : EvalM Val := do
       | .bool true  => e.eval fuel
       | .bool false => t.eval fuel
       | _ => throw "Boolean expected"
-    | «while» c b =>
+    | .while c b =>
       match (← evalExpr c) with
       | .bool true  => b.eval fuel; stmt.eval fuel
       | .bool false => return ()
@@ -324,10 +324,10 @@ instance : Repr State where
     | .val (.bool true) => e.simplify
     | .val (.bool false) => t.simplify
     | c' => ite c' e.simplify t.simplify
-  | «while» c b =>
+  | .while c b =>
     match c.simplify with
     | .val (.bool false) => skip
-    | c' => «while» c' b.simplify
+    | c' => .while c' b.simplify
 
 def example3 := `[Stmt|
   if (1 < 2 + 3) {
@@ -413,7 +413,7 @@ local notation "⊥" => []
   | ite c s₁ s₂ =>
     match s₁.constProp σ, s₂.constProp σ with
     | (s₁', σ₁), (s₂', σ₂) => (ite (c.constProp σ) s₁' s₂', σ₁.join σ₂)
-  | «while» c b => («while» (c.constProp ⊥) (b.constProp ⊥).1, ⊥)
+  | .while c b => (.while (c.constProp ⊥) (b.constProp ⊥).1, ⊥)
 
 def State.le (σ₁ σ₂ : State) : Prop :=
   ∀ ⦃x : Var⦄ ⦃v : Val⦄, σ₁.find? x = some v → σ₂.find? x = some v