diff --git a/doc/BoolExpr.lean b/doc/BoolExpr.lean
index 58951671aa..a5cb9010ea 100644
--- a/doc/BoolExpr.lean
+++ b/doc/BoolExpr.lean
@@ -104,9 +104,9 @@ syntax entry := ident " ↦ " term:max
 syntax entry,* "⊢" term : term
 
 macro_rules
-  | `( $[$xs:ident ↦ $vs:term],* ⊢ $p:term ) =>
+  | `( $[$xs ↦ $vs],* ⊢ $p) =>
     let xs := xs.map fun x => quote x.getId.toString
-    `(denote (List.toAssocList [$[( $xs , $vs )],*]) `[BExpr| $p])
+    `(denote (List.toAssocList [$[($xs, $vs)],*]) `[BExpr| $p])
 
 #check b ↦ true ⊢ b ∨ b
 #eval  a ↦ false, b ↦ false ⊢ b ∨ a
diff --git a/doc/examples/bintree.lean b/doc/examples/bintree.lean
index b75fa17bed..9b92366388 100644
--- a/doc/examples/bintree.lean
+++ b/doc/examples/bintree.lean
@@ -176,10 +176,10 @@ The modifier `local` specifies the scope of the macro.
 /-- The `have_eq lhs rhs` tactic (tries to) prove that `lhs = rhs`,
     and then replaces `lhs` with `rhs`. -/
 local macro "have_eq " lhs:term:max rhs:term:max : tactic =>
-  `((have h : $lhs:term = $rhs:term :=
+  `((have h : $lhs = $rhs :=
        -- TODO: replace with linarith
        by simp_arith at *; apply Nat.le_antisymm <;> assumption
-     try subst $lhs:term))
+     try subst $lhs))
 
 /-!
 The `by_cases' e` is just the regular `by_cases` followed by `simp` using all
@@ -191,7 +191,7 @@ useful if `e` is the condition of an `if`-statement.
 -/
 /-- `by_cases' e` is a shorthand form `by_cases e <;> simp[*]` -/
 local macro "by_cases' " e:term :  tactic =>
-  `(by_cases $e:term <;> simp [*])
+  `(by_cases $e <;> simp [*])
 
 
 /-!
diff --git a/doc/metaprogramming-arith.lean b/doc/metaprogramming-arith.lean
index 92763d78f6..ee1b6c5d92 100644
--- a/doc/metaprogramming-arith.lean
+++ b/doc/metaprogramming-arith.lean
@@ -18,9 +18,9 @@ syntax "`[Arith| " arith "]" : term
 macro_rules
   | `(`[Arith| $s:str]) => `(Arith.symbol $s)
   | `(`[Arith| $num:num]) => `(Arith.int $num)
-  | `(`[Arith| $x:arith + $y:arith]) => `(Arith.add `[Arith| $x] `[Arith| $y])
-  | `(`[Arith| $x:arith * $y:arith]) => `(Arith.mul `[Arith| $x] `[Arith| $y])
-  | `(`[Arith| ($x:arith)]) => `(`[Arith| $x])
+  | `(`[Arith| $x + $y]) => `(Arith.add `[Arith| $x] `[Arith| $y])
+  | `(`[Arith| $x * $y]) => `(Arith.mul `[Arith| $x] `[Arith| $y])
+  | `(`[Arith| ($x)]) => `(`[Arith| $x])
 
 #check `[Arith| "x" * "y"]  -- mul
 -- Arith.mul (Arith.symbol "x") (Arith.symbol "y")
diff --git a/src/Init/Classical.lean b/src/Init/Classical.lean
index 83e72ce853..480eb14d4c 100644
--- a/src/Init/Classical.lean
+++ b/src/Init/Classical.lean
@@ -129,14 +129,14 @@ theorem byContradiction {p : Prop} (h : ¬p → False) : p :=
 syntax "by_cases" (atomic(ident ":"))? term : tactic
 
 macro_rules
-  | `(tactic| by_cases $h:ident : $e:term) =>
+  | `(tactic| by_cases $h : $e) =>
     `(tactic|
-      cases em $e:term with
-      | inl $h:ident => _
-      | inr $h:ident => _)
-  | `(tactic| by_cases $e:term) =>
+      cases em $e with
+      | inl $h => _
+      | inr $h => _)
+  | `(tactic| by_cases $e) =>
     `(tactic|
-      cases em $e:term with
+      cases em $e with
       | inl h => _
       | inr h => _)
 
diff --git a/src/Init/Conv.lean b/src/Init/Conv.lean
index ad15eea968..d2bcae0158 100644
--- a/src/Init/Conv.lean
+++ b/src/Init/Conv.lean
@@ -47,24 +47,22 @@ syntax (name := paren) "(" convSeq ")" : conv
 syntax (name := convConvSeq) "conv " " => " convSeq : conv
 
 /-- `· conv` focuses on the main conv goal and tries to solve it using `s` -/
-macro dot:("·" <|> ".") s:convSeq : conv => `({%$dot ($s:convSeq) })
-macro "rw " c:(config)? s:rwRuleSeq : conv => `(rewrite $[$c:config]? $s:rwRuleSeq)
-macro "erw " s:rwRuleSeq : conv => `(rw (config := { transparency := Meta.TransparencyMode.default }) $s:rwRuleSeq)
+macro dot:("·" <|> ".") s:convSeq : conv => `({%$dot ($s) })
+macro "rw " c:(config)? s:rwRuleSeq : conv => `(rewrite $[$c]? $s)
+macro "erw " s:rwRuleSeq : conv => `(rw (config := { transparency := Meta.TransparencyMode.default }) $s)
 
 macro "args" : conv => `(congr)
 macro "left" : conv => `(lhs)
 macro "right" : conv => `(rhs)
-syntax "intro " (colGt ident)* : conv
-macro_rules
-  | `(conv| intro $[$xs:ident]*) => `(conv| ext $xs*)
+macro "intro " xs:(colGt ident)* : conv => `(conv| ext $xs*)
 
 syntax enterArg := ident <|> ("@"? num)
 syntax "enter " "[" (colGt enterArg),+ "]": conv
 macro_rules
   | `(conv| enter [$i:num]) => `(conv| arg $i)
-  | `(conv| enter [@$i:num]) => `(conv| arg @$i)
+  | `(conv| enter [@$i]) => `(conv| arg @$i)
   | `(conv| enter [$id:ident]) => `(conv| ext $id)
-  | `(conv| enter [$arg:enterArg, $args,*]) => `(conv| (enter [$arg]; enter [$args,*]))
+  | `(conv| enter [$arg, $args,*]) => `(conv| (enter [$arg]; enter [$args,*]))
 
 macro "skip" : conv => `(tactic => rfl)
 macro "done" : conv => `(tactic' => done)
diff --git a/src/Init/Meta.lean b/src/Init/Meta.lean
index 154ed3a6b8..2a63b80f4c 100644
--- a/src/Init/Meta.lean
+++ b/src/Init/Meta.lean
@@ -1253,7 +1253,7 @@ end Meta
 namespace Parser.Tactic
 
 macro "erw " s:rwRuleSeq loc:(location)? : tactic =>
-  `(rw (config := { transparency := Lean.Meta.TransparencyMode.default }) $s:rwRuleSeq $[$loc:location]?)
+  `(rw (config := { transparency := Lean.Meta.TransparencyMode.default }) $s $(loc)?)
 
 syntax simpAllKind := atomic("(" &"all") " := " &"true" ")"
 syntax dsimpKind   := atomic("(" &"dsimp") " := " &"true" ")"
@@ -1261,18 +1261,18 @@ syntax dsimpKind   := atomic("(" &"dsimp") " := " &"true" ")"
 macro "declare_simp_like_tactic" opt:((simpAllKind <|> dsimpKind)?) tacName:ident tacToken:str updateCfg:term : command => do
   let (kind, tkn, stx) ←
     if opt.raw.isNone then
-      pure (← `(``simp), ← `("simp "), ← `(syntax (name := $tacName:ident) $tacToken:str (config)? (discharger)? (&"only ")? ("[" (simpStar <|> simpErase <|> simpLemma),* "]")? (location)? : tactic))
+      pure (← `(``simp), ← `("simp "), ← `(syntax (name := $tacName) $tacToken:str (config)? (discharger)? (&"only ")? ("[" (simpStar <|> simpErase <|> simpLemma),* "]")? (location)? : tactic))
     else if opt.raw[0].getKind == ``simpAllKind then
-      pure (← `(``simpAll), ← `("simp_all "), ← `(syntax (name := $tacName:ident) $tacToken:str (config)? (discharger)? (&"only ")? ("[" (simpErase <|> simpLemma),* "]")? : tactic))
+      pure (← `(``simpAll), ← `("simp_all "), ← `(syntax (name := $tacName) $tacToken:str (config)? (discharger)? (&"only ")? ("[" (simpErase <|> simpLemma),* "]")? : tactic))
     else
-      pure (← `(``dsimp), ← `("dsimp "), ← `(syntax (name := $tacName:ident) $tacToken:str (config)? (discharger)? (&"only ")? ("[" (simpErase <|> simpLemma),* "]")? (location)? : tactic))
+      pure (← `(``dsimp), ← `("dsimp "), ← `(syntax (name := $tacName) $tacToken:str (config)? (discharger)? (&"only ")? ("[" (simpErase <|> simpLemma),* "]")? (location)? : tactic))
   `($stx:command
-    @[macro $tacName:ident] def expandSimp : Macro := fun s => do
+    @[macro $tacName] def expandSimp : Macro := fun s => do
       let c ← match s[1][0] with
-        | `(config| (config := $$c:term)) => `(config| (config := $updateCfg:term $$c))
-        | _ => `(config| (config := $updateCfg:term {}))
-      let s := s.setKind $kind:term
-      let s := s.setArg 0 (mkAtomFrom s[0] $tkn:term)
+        | `(config| (config := $$c)) => `(config| (config := $updateCfg $$c))
+        | _ => `(config| (config := $updateCfg {}))
+      let s := s.setKind $kind
+      let s := s.setArg 0 (mkAtomFrom s[0] $tkn)
       let r := s.setArg 1 (mkNullNode #[c])
       return r)
 
diff --git a/src/Init/NotationExtra.lean b/src/Init/NotationExtra.lean
index c714fbc43e..a750ece2da 100644
--- a/src/Init/NotationExtra.lean
+++ b/src/Init/NotationExtra.lean
@@ -29,7 +29,7 @@ def expandExplicitBindersAux (combinator : Syntax) (idents : Array Syntax) (type
       let ident := idents[i]![0]
       let acc ← match ident.isIdent, type? with
         | true,  none      => `($combinator fun $ident => $acc)
-        | true,  some type => `($combinator fun $ident:ident : $type => $acc)
+        | true,  some type => `($combinator fun $ident : $type => $acc)
         | false, none      => `($combinator fun _ => $acc)
         | false, some type => `($combinator fun _ : $type => $acc)
       loop i acc
@@ -67,12 +67,12 @@ syntax unifConstraintElem := colGe unifConstraint ", "?
 syntax (docComment)? attrKind "unif_hint " (ident)? bracketedBinder* " where " withPosition(unifConstraintElem*) ("|-" <|> "⊢ ") unifConstraint : command
 
 macro_rules
-  | `($[$doc?:docComment]? $kind:attrKind unif_hint $(n)? $bs* where $[$cs₁:term ≟ $cs₂]* |- $t₁:term ≟ $t₂) => do
+  | `($[$doc?:docComment]? $kind:attrKind unif_hint $(n)? $bs* where $[$cs₁ ≟ $cs₂]* |- $t₁ ≟ $t₂) => do
     let mut body ← `($t₁ = $t₂)
     for (c₁, c₂) in cs₁.zip cs₂ |>.reverse do
       body ← `($c₁ = $c₂ → $body)
     let hint : Ident ← `(hint)
-    `($[$doc?:docComment]? @[$kind:attrKind unificationHint] def $(n.getD hint) $bs:bracketedBinder* : Sort _ := $body)
+    `($[$doc?:docComment]? @[$kind unificationHint] def $(n.getD hint) $bs* : Sort _ := $body)
 end Lean
 
 open Lean
@@ -224,13 +224,13 @@ syntax declModifiers "class " "abbrev " declId bracketedBinder* (":" term)?
 macro_rules
   | `($mods:declModifiers class abbrev $id $params* $[: $ty]? := $[ $parents $[,]? ]*) =>
     let ctor := mkIdentFrom id <| id.raw[0].getId.modifyBase (. ++ `mk)
-    `($mods:declModifiers class $id $params* extends $[$parents:term],* $[: $ty]?
+    `($mods:declModifiers class $id $params* extends $parents,* $[: $ty]?
       attribute [instance] $ctor)
 
 /-- `· tac` focuses on the main goal and tries to solve it using `tac`, or else fails. -/
 syntax ("·" <|> ".") ppHardSpace many1Indent(tactic ";"? ppLine) : tactic
 macro_rules
-  | `(tactic| ·%$dot $[$tacs:tactic $[;%$sc]?]*) => `(tactic| {%$dot $[$tacs:tactic $[;%$sc]?]*})
+  | `(tactic| ·%$dot $[$tacs $[;%$sc]?]*) => `(tactic| {%$dot $[$tacs $[;%$sc]?]*})
 
 /--
   Similar to `first`, but succeeds only if one the given tactics solves the current goal.
diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean
index a197f85805..05c63eca84 100644
--- a/src/Init/Tactics.lean
+++ b/src/Init/Tactics.lean
@@ -205,7 +205,7 @@ syntax (name := rewriteSeq) "rewrite " (config)? rwRuleSeq (location)? : tactic
 -/
 macro (name := rwSeq) rw:"rw " c:(config)? s:rwRuleSeq l:(location)? : tactic =>
   match s with
-  | `(rwRuleSeq| [%$lbrak $rs:rwRule,* ]%$rbrak) =>
+  | `(rwRuleSeq| [%$lbrak $rs,* ]%$rbrak) =>
     -- We show the `rfl` state on `]`
     `(tactic| rewrite%$rw $(c)? [%$lbrak $rs,*] $(l)?; try (with_reducible rfl%$rbrak))
   | _ => Macro.throwUnsupported
@@ -280,7 +280,7 @@ macro "have " d:haveDecl : tactic => `(refine_lift have $d:haveDecl; ?_)
 /--
 `have h := e` adds the hypothesis `h : t` if `e : t`.
 -/
-macro (priority := high) "have" x:ident " := " p:term : tactic => `(have $x:ident : _ := $p)
+macro (priority := high) "have" x:ident " := " p:term : tactic => `(have $x : _ := $p)
 /--
 Given a main goal `ctx |- t`, `suffices h : t' from e` replaces the main goal with `ctx |- t'`,
 `e` must have type `t` in the context `ctx, h : t'`.
@@ -288,7 +288,7 @@ Given a main goal `ctx |- t`, `suffices h : t' from e` replaces the main goal wi
 The variant `suffices h : t' by tac` is a shorthand for `suffices h : t' from by tac`.
 If `h :` is omitted, the name `this` is used.
  -/
-macro "suffices " d:sufficesDecl : tactic => `(refine_lift suffices $d:sufficesDecl; ?_)
+macro "suffices " d:sufficesDecl : tactic => `(refine_lift suffices $d; ?_)
 /--
 `let h : t := e` adds the hypothesis `h : t := e` to the current goal if `e` a term of type `t`.
 If `t` is omitted, it will be inferred.
@@ -300,15 +300,15 @@ macro "let " d:letDecl : tactic => `(refine_lift let $d:letDecl; ?_)
 `show t` finds the first goal whose target unifies with `t`. It makes that the main goal,
  performs the unification, and replaces the target with the unified version of `t`.
 -/
-macro "show " e:term : tactic => `(refine_lift show $e:term from ?_) -- TODO: fix, see comment
+macro "show " e:term : tactic => `(refine_lift show $e from ?_) -- TODO: fix, see comment
 syntax (name := letrec) withPosition(atomic("let " &"rec ") letRecDecls) : tactic
 macro_rules
-  | `(tactic| let rec $d:letRecDecls) => `(tactic| refine_lift let rec $d:letRecDecls; ?_)
+  | `(tactic| let rec $d) => `(tactic| refine_lift let rec $d; ?_)
 
 -- Similar to `refineLift`, but using `refine'`
 macro "refine_lift' " e:term : tactic => `(focus (refine' no_implicit_lambda% $e; rotate_right))
 macro "have' " d:haveDecl : tactic => `(refine_lift' have $d:haveDecl; ?_)
-macro (priority := high) "have'" x:ident " := " p:term : tactic => `(have' $x:ident : _ := $p)
+macro (priority := high) "have'" x:ident " := " p:term : tactic => `(have' $x : _ := $p)
 macro "let' " d:letDecl : tactic => `(refine_lift' let $d:letDecl; ?_)
 
 syntax inductionAltLHS := "| " (("@"? ident) <|> "_") (ident <|> "_")*
@@ -397,7 +397,7 @@ macro_rules | `(tactic| trivial) => `(tactic| decide)
 macro_rules | `(tactic| trivial) => `(tactic| apply True.intro)
 macro_rules | `(tactic| trivial) => `(tactic| apply And.intro <;> trivial)
 
-macro "unhygienic " t:tacticSeq : tactic => `(set_option tactic.hygienic false in $t:tacticSeq)
+macro "unhygienic " t:tacticSeq : tactic => `(set_option tactic.hygienic false in $t)
 
 /-- `fail msg` is a tactic that always fail and produces an error using the given message. -/
 syntax (name := fail) "fail " (str)? : tactic
diff --git a/src/Init/WFTactics.lean b/src/Init/WFTactics.lean
index e26d725e95..0d7a53f568 100644
--- a/src/Init/WFTactics.lean
+++ b/src/Init/WFTactics.lean
@@ -22,7 +22,7 @@ macro "decreasing_with " ts:tacticSeq : tactic =>
     repeat (first | apply Prod.Lex.right | apply Prod.Lex.left)
     repeat (first | apply PSigma.Lex.right | apply PSigma.Lex.left)
     first
-    | $ts:tacticSeq
+    | $ts
     | fail "failed to prove termination, possible solutions:\n  - Use `have`-expressions to prove the remaining goals\n  - Use `termination_by` to specify a different well-founded relation\n  - Use `decreasing_by` to specify your own tactic for discharging this kind of goal"))
 
 macro "decreasing_tactic" : tactic => `(decreasing_with first | decreasing_trivial | subst_vars; decreasing_trivial)
diff --git a/src/Lean/Elab/BuiltinNotation.lean b/src/Lean/Elab/BuiltinNotation.lean
index cae20f5348..071f412d42 100644
--- a/src/Lean/Elab/BuiltinNotation.lean
+++ b/src/Lean/Elab/BuiltinNotation.lean
@@ -75,23 +75,23 @@ are turned into a new anonymous constructor application. For example,
 
 @[builtinMacro Lean.Parser.Term.show] def expandShow : Macro := fun stx =>
   match stx with
-  | `(show $type from $val)            => let thisId := mkIdentFrom stx `this; `(let_fun $thisId : $type := $val; $thisId)
-  | `(show $type by%$b $tac:tacticSeq) => `(show $type from by%$b $tac:tacticSeq)
-  | _                                  => Macro.throwUnsupported
+  | `(show $type from $val)  => let thisId := mkIdentFrom stx `this; `(let_fun $thisId : $type := $val; $thisId)
+  | `(show $type by%$b $tac) => `(show $type from by%$b $tac)
+  | _                        => Macro.throwUnsupported
 
 @[builtinMacro Lean.Parser.Term.have] def expandHave : Macro := fun stx =>
   let thisId := mkIdentFrom stx `this
   match stx with
   | `(have $x $bs* $[: $type]? := $val; $body)            => `(let_fun $x $bs* $[: $type]? := $val; $body)
-  | `(have $[: $type]? := $val; $body)                    => `(have $thisId:ident $[: $type]? := $val; $body)
-  | `(have $x $bs* $[: $type]? $alts:matchAlts; $body)    => `(let_fun $x $bs* $[: $type]? $alts:matchAlts; $body)
-  | `(have $[: $type]? $alts:matchAlts; $body)            => `(have $thisId:ident $[: $type]? $alts:matchAlts; $body)
+  | `(have $[: $type]? := $val; $body)                    => `(have $thisId $[: $type]? := $val; $body)
+  | `(have $x $bs* $[: $type]? $alts; $body)              => `(let_fun $x $bs* $[: $type]? $alts; $body)
+  | `(have $[: $type]? $alts:matchAlts; $body)            => `(have $thisId $[: $type]? $alts:matchAlts; $body)
   | `(have $pattern:term $[: $type]? := $val:term; $body) => `(let_fun $pattern:term $[: $type]? := $val:term ; $body)
-  | _                                                          => Macro.throwUnsupported
+  | _                                                     => Macro.throwUnsupported
 
 @[builtinMacro Lean.Parser.Term.suffices] def expandSuffices : Macro
   | `(suffices $[$x :]? $type from $val; $body)            => `(have $[$x]? : $type := $body; $val)
-  | `(suffices $[$x :]? $type by%$b $tac:tacticSeq; $body) => `(have $[$x]? : $type := $body; by%$b $tac:tacticSeq)
+  | `(suffices $[$x :]? $type by%$b $tac:tacticSeq; $body) => `(have $[$x]? : $type := $body; by%$b $tac)
   | _                                                           => Macro.throwUnsupported
 
 open Lean.Parser in
@@ -224,12 +224,12 @@ def elabCDotFunctionAlias? (stx : Term) : TermElabM (Option Expr) := do
   let some stx ← liftMacroM <| expandCDotArg? stx | pure none
   let stx ← liftMacroM <| expandMacros stx
   match stx with
-  | `(fun $binders* => $f:ident $args*) =>
+  | `(fun $binders* => $f $args*) =>
     if binders == args then
       try Term.resolveId? f catch _ => return none
     else
       return none
-  | `(fun $binders* => binop% $f:ident $a $b) =>
+  | `(fun $binders* => binop% $f $a $b) =>
     if binders == #[a, b] then
       try Term.resolveId? f catch _ => return none
     else
diff --git a/src/Lean/Elab/Declaration.lean b/src/Lean/Elab/Declaration.lean
index 4952d0a005..e9492764c0 100644
--- a/src/Lean/Elab/Declaration.lean
+++ b/src/Lean/Elab/Declaration.lean
@@ -179,7 +179,7 @@ def elabDeclaration : CommandElab := fun stx => do
   match (← liftMacroM <| expandDeclNamespace? stx) with
   | some (ns, newStx) => do
     let ns := mkIdentFrom stx ns
-    let newStx ← `(namespace $ns:ident $(⟨newStx⟩) end $ns:ident)
+    let newStx ← `(namespace $ns $(⟨newStx⟩) end $ns)
     withMacroExpansion stx newStx <| elabCommand newStx
   | none => do
     let decl     := stx[1]
@@ -259,7 +259,7 @@ def expandMutualNamespace : Macro := fun stx => do
   | some ns =>
     let ns := mkIdentFrom stx ns
     let stxNew := stx.setArg 1 (mkNullNode elemsNew)
-    `(namespace $ns:ident $(⟨stxNew⟩) end $ns:ident)
+    `(namespace $ns $(⟨stxNew⟩) end $ns)
   | none => Macro.throwUnsupported
 
 @[builtinMacro Lean.Parser.Command.mutual]
diff --git a/src/Lean/Elab/MacroRules.lean b/src/Lean/Elab/MacroRules.lean
index 57c0f5e524..2c6947dcde 100644
--- a/src/Lean/Elab/MacroRules.lean
+++ b/src/Lean/Elab/MacroRules.lean
@@ -35,7 +35,7 @@ def elabMacroRulesAux (doc? : Option (TSyntax ``docComment)) (attrKind : TSyntax
       else
         throwErrorAt alt "invalid macro_rules alternative, unexpected syntax node kind '{k'}'"
     | _ => throwUnsupportedSyntax
-  `($[$doc?:docComment]? @[$attrKind:attrKind macro $(Lean.mkIdent k)]
+  `($[$doc?:docComment]? @[$attrKind macro $(Lean.mkIdent k)]
     aux_def macroRules $(mkIdentFrom tk k) : Macro :=
      fun $alts:matchAlt* | _ => throw Lean.Macro.Exception.unsupportedSyntax)
 
diff --git a/src/Lean/Elab/Match.lean b/src/Lean/Elab/Match.lean
index dc239f1441..dff9a659b3 100644
--- a/src/Lean/Elab/Match.lean
+++ b/src/Lean/Elab/Match.lean
@@ -927,7 +927,7 @@ where
             return mkHole ref
           else
             let id := mkIdentFrom ref localDecl.userName
-            `(?$id:ident)
+            `(?$id)
         else
           return mkHole ref
       let altViews  := altViews.map fun altView => { altView with patterns := wildcards ++ altView.patterns }
@@ -1148,7 +1148,7 @@ private def expandNonAtomicDiscrs? (matchStx : Syntax) : TermElabM (Option Synta
               throwError "unexpected internal auxiliary discriminant name"
             let discrNew := discr.setArg 1 d
             let r ← loop discrs (discrsNew.push discrNew) foundFVars
-            `(let $d:ident := $term; $r)
+            `(let $d := $term; $r)
           match (← isAtomicDiscr? term) with
           | some x  => if x.isFVar then loop discrs (discrsNew.push discr) (foundFVars.insert x.fvarId!) else addAux
           | none    => addAux
@@ -1252,7 +1252,7 @@ matched on in dependent variables' types. Use `match (generalizing := true) ...`
 enforce this. -/
 @[builtinTermElab «match»] def elabMatch : TermElab := fun stx expectedType? => do
   match stx with
-  | `(match $discr:term with | $y:ident => $rhs:term) =>
+  | `(match $discr:term with | $y:ident => $rhs) =>
      if (← isPatternVar y) then expandSimpleMatch stx discr y rhs expectedType? else elabMatchDefault stx expectedType?
   | _ => elabMatchDefault stx expectedType?
 where
@@ -1286,7 +1286,7 @@ e.g. because it has no constructors. -/
       elabMatchAux none #[discr] #[] mkNullNode expectedType
     | _ =>
       let d ← mkAuxDiscr
-      let stxNew ← `(let $d:ident := $discrExpr; nomatch $d:ident)
+      let stxNew ← `(let $d := $discrExpr; nomatch $d)
       withMacroExpansion stx stxNew <| elabTerm stxNew expectedType?
   | _ => throwUnsupportedSyntax
 
diff --git a/src/Lean/Elab/Notation.lean b/src/Lean/Elab/Notation.lean
index be2205c7c2..bb95e4fdfa 100644
--- a/src/Lean/Elab/Notation.lean
+++ b/src/Lean/Elab/Notation.lean
@@ -94,7 +94,7 @@ def mkSimpleDelab (attrKind : TSyntax ``attrKind) (pat qrhs : Term) : OptionT Ma
   -- The reference is attached to the syntactic representation of the called function itself, not the entire function application
   let lhs ← `($$f:ident)
   let lhs := Syntax.mkApp lhs (.mk args)
-  `(@[$attrKind:attrKind appUnexpander $(mkIdent c):ident]
+  `(@[$attrKind appUnexpander $(mkIdent c)]
     aux_def unexpand $(mkIdent c) : Lean.PrettyPrinter.Unexpander := fun
       | `($lhs) => withRef f `($pat)
       | _       => throw ())
@@ -123,7 +123,7 @@ private def expandNotationAux (ref : Syntax)
      So, we must include current namespace when we create a pattern for the following `macro_rules` commands. -/
   let fullName := currNamespace ++ name
   let pat : Term := ⟨mkNode fullName patArgs⟩
-  let stxDecl ← `($attrKind:attrKind syntax $[: $prec?]? (name := $(mkIdent name)) (priority := $(quote prio):num) $[$syntaxParts]* : $cat)
+  let stxDecl ← `($attrKind:attrKind syntax $[: $prec?]? (name := $(mkIdent name)) (priority := $(quote prio)) $[$syntaxParts]* : $cat)
   let macroDecl ← `(macro_rules | `($pat) => ``($qrhs))
   let macroDecls ←
     if isLocalAttrKind attrKind then
diff --git a/src/Lean/PrettyPrinter/Delaborator/Basic.lean b/src/Lean/PrettyPrinter/Delaborator/Basic.lean
index 205c76a9b8..b5928e0ab9 100644
--- a/src/Lean/PrettyPrinter/Delaborator/Basic.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/Basic.lean
@@ -251,7 +251,7 @@ partial def delab : Delab := do
   let stx ← delabFor k <|> (liftM $ show MetaM _ from throwError "don't know how to delaborate '{k}'")
   if ← getPPOption getPPAnalyzeTypeAscriptions <&&> getPPOption getPPAnalysisNeedsType <&&> pure !e.isMData then
     let typeStx ← withType delab
-    `(($stx:term : $typeStx:term)) >>= annotateCurPos
+    `(($stx : $typeStx)) >>= annotateCurPos
   else
     return stx
 
diff --git a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
index 9c835ad229..58052a6f6a 100644
--- a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
@@ -233,7 +233,7 @@ def unexpandStructureInstance (stx : Syntax) : Delab := whenPPOption getPPStruct
     let fieldPos ← nextExtraPos
     let fieldId := annotatePos fieldPos fieldId
     addFieldInfo fieldPos (s.induct ++ fieldName) fieldName fieldId fieldVals[idx]!
-    let field ← `(structInstField|$fieldId:ident := $(stx[1][idx]):term)
+    let field ← `(structInstField|$fieldId:ident := $(stx[1][idx]))
     fields := fields.push field
   let tyStx ← withType do
     if (← getPPOption getPPStructureInstanceType) then delab >>= pure ∘ some else pure none
@@ -262,7 +262,7 @@ def delabAppImplicit : Delab := do
       let arg ← getExpr
       let opts ← getOptions
       let mkNamedArg (name : Name) (argStx : Syntax) : DelabM Syntax := do
-        `(Parser.Term.namedArgument| ($(mkIdent name):ident := $argStx:term))
+        `(Parser.Term.namedArgument| ($(mkIdent name) := $argStx))
       let argStx? : Option Syntax ←
         if ← getPPOption getPPAnalysisSkip then pure none
         else if ← getPPOption getPPAnalysisHole then `(_)
@@ -395,7 +395,7 @@ def delabAppMatch : Delab := whenPPOption getPPNotation <| whenPPOption getPPMat
         if let some hName := st.info.discrInfos[idx]!.hName? then
           -- TODO: we should check whether the corresponding binder name, matches `hName`.
           -- If it does not we should pretty print this `match` as a regular application.
-          return { st with discrs := st.discrs.push (← `(matchDiscr| $(mkIdent hName):ident : $discr:term)) }
+          return { st with discrs := st.discrs.push (← `(matchDiscr| $(mkIdent hName) : $discr)) }
         else
           return { st with discrs := st.discrs.push (← `(matchDiscr| $discr:term)) }
       else if st.rhss.size < st.info.altNumParams.size then
diff --git a/src/Lean/Server/FileWorker/RequestHandling.lean b/src/Lean/Server/FileWorker/RequestHandling.lean
index d0cb015be5..a5b0826819 100644
--- a/src/Lean/Server/FileWorker/RequestHandling.lean
+++ b/src/Lean/Server/FileWorker/RequestHandling.lean
@@ -256,12 +256,12 @@ where
         unless stx.isOfKind ``Lean.Parser.Command.declaration do
           return (syms, stxs')
         if let some stxRange := stx.getRange? then
-          let (name, selection) : String × Syntax := match stx with
-            | `($_:declModifiers $_:attrKind instance $[$np:namedPrio]? $[$id:ident$[.{$ls,*}]?]? $sig:declSig $_) =>
+          let (name, selection) := match stx with
+            | `($_:declModifiers $_:attrKind instance $[$np:namedPrio]? $[$id$[.{$ls,*}]?]? $sig:declSig $_) =>
               ((·.getId.toString) <$> id |>.getD s!"instance {sig.raw.reprint.getD ""}", id.map (·.raw) |>.getD sig)
             | _ =>
               match stx.getArg 1 |>.getArg 1 with
-              | `(declId|$id:ident$[.{$ls,*}]?) => (id.raw.getId.toString, id)
+              | `(declId|$id$[.{$ls,*}]?) => (id.raw.getId.toString, id)
               | _ =>
                 let stx10 : Syntax := (stx.getArg 1).getArg 0 -- TODO: stx[1][0] times out
                 (stx10.isIdOrAtom?.getD "<unknown>", stx10)
diff --git a/src/Lean/Server/Rpc/Deriving.lean b/src/Lean/Server/Rpc/Deriving.lean
index 8ad3231d07..05f33cd43b 100644
--- a/src/Lean/Server/Rpc/Deriving.lean
+++ b/src/Lean/Server/Rpc/Deriving.lean
@@ -20,9 +20,9 @@ private def deriveWithRefInstance (typeNm : Name) : CommandElabM Bool := do
   -- TODO(WN): check that `typeNm` is not a scalar type
   let typeId := mkIdent typeNm
   let cmds ← `(
-    unsafe def unsafeInst : RpcEncoding (WithRpcRef $typeId:ident) Lsp.RpcRef where
+    unsafe def unsafeInst : RpcEncoding (WithRpcRef $typeId) Lsp.RpcRef where
       rpcEncode := WithRpcRef.encodeUnsafe $(quote typeNm)
-      rpcDecode := WithRpcRef.decodeUnsafeAs $typeId:ident $(quote typeNm)
+      rpcDecode := WithRpcRef.decodeUnsafeAs $typeId $(quote typeNm)
 
     @[implementedBy unsafeInst]
     opaque inst : RpcEncoding (WithRpcRef $typeId) Lsp.RpcRef
@@ -97,7 +97,7 @@ private def deriveStructureInstance (indVal : InductiveVal) (params : Array Expr
 
     -- helpers for field initialization syntax
     let fieldInits (func : Name) := fieldIds.mapM fun fid =>
-      `(Parser.Term.structInstField| $fid:ident := ← $(mkIdent func):ident a.$fid:ident)
+      `(Parser.Term.structInstField| $fid:ident := ← $(mkIdent func) a.$fid)
     let encInits ← fieldInits ``rpcEncode
     let decInits ← fieldInits ``rpcDecode
 
diff --git a/tests/lean/run/liftMethodInMacrosIssue.lean b/tests/lean/run/liftMethodInMacrosIssue.lean
index fed37edf66..9792196ce8 100644
--- a/tests/lean/run/liftMethodInMacrosIssue.lean
+++ b/tests/lean/run/liftMethodInMacrosIssue.lean
@@ -19,7 +19,7 @@ else
 syntax term "<|||>" term : doElem
 
 macro_rules
-| `(doElem| $a:term <|||> $b:term) => `(doElem| if (← $a:term) then pure true else $b:term)
+| `(doElem| $a:term <|||> $b) => `(doElem| if (← $a) then pure true else $b:term)
 
 def tst2 : IO Bool := do
 pure true <|||> (← throw $ IO.userError "failed")
diff --git a/tests/lean/run/obtain.lean b/tests/lean/run/obtain.lean
index 875169f969..15fa632091 100644
--- a/tests/lean/run/obtain.lean
+++ b/tests/lean/run/obtain.lean
@@ -1,7 +1,7 @@
 
 
 macro "obtain " p:term " from " d:term "; " body:term : term =>
-`(match $d:term with | $p:term => $body:term)
+`(match $d:term with | $p => $body)
 
 theorem tst1 {p q r} (h : p ∧ q ∧ r) : q ∧ p ∧ r :=
 match h with
@@ -12,7 +12,7 @@ obtain ⟨h₁, ⟨h₂, h₃⟩⟩ from h;
 ⟨h₂, ⟨h₁, h₃⟩⟩
 
 macro "obtain " p:term " from " d:term : tactic =>
-`(tactic| match $d:term with | $p:term => ?hole)
+`(tactic| match $d:term with | $p => ?hole)
 
 theorem tst3 {p q r} (h : p ∧ q ∧ r) : q ∧ p ∧ r := by
   obtain ⟨h₁, ⟨h₂, h₃⟩⟩ from h