diff --git a/src/Lean/Elab/Binders.lean b/src/Lean/Elab/Binders.lean
index 1c6494f68b..c996ac4557 100644
--- a/src/Lean/Elab/Binders.lean
+++ b/src/Lean/Elab/Binders.lean
@@ -498,14 +498,15 @@ def expandMatchAltsWhereDecls (matchAltsWhereDecls : Syntax) : MacroM Syntax :=
       `(@fun x => $body)
   loop (getMatchAltsNumPatterns matchAlts) #[]
 
-@[builtinMacro Lean.Parser.Term.fun] partial def expandFun : Macro
+@[builtinMacro Lean.Parser.Term.fun] partial def expandFun : Macro := fun stx =>
+  match stx with
   | `(fun $binders* => $body) => do
     let (binders, body, expandedPattern) ← expandFunBinders binders body
     if expandedPattern then
       `(fun $binders* => $body)
     else
       Macro.throwUnsupported
-  | stx@`(fun $m:matchAlts) => expandMatchAltsIntoMatch stx m
+  | `(fun $m:matchAlts) => expandMatchAltsIntoMatch stx m
   | _ => Macro.throwUnsupported
 
 open Lean.Elab.Term.Quotation in
diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean
index 9da37787e6..a4f850a124 100644
--- a/src/Lean/Elab/MutualDef.lean
+++ b/src/Lean/Elab/MutualDef.lean
@@ -164,8 +164,9 @@ private def expandWhereStructInst : Macro
       | `(letDecl|$decl:letEqnsDecl) => expandLetEqnsDecl decl
       | `(letDecl|$decl:letIdDecl)   => pure decl
       | _                               => Macro.throwUnsupported
-    let structInstFields ← letIdDecls.mapM fun
-      | stx@`(letIdDecl|$id:ident $[$binders]* $[: $ty?]? := $val) => withRef stx do
+    let structInstFields ← letIdDecls.mapM fun stx =>
+      match stx with
+      | `(letIdDecl|$id:ident $[$binders]* $[: $ty?]? := $val) => withRef stx do
         let mut val := val
         if let some ty := ty? then
           val ← `(($val : $ty))
diff --git a/src/Lean/Elab/Notation.lean b/src/Lean/Elab/Notation.lean
index 0fdfa85856..0b187fa0a5 100644
--- a/src/Lean/Elab/Notation.lean
+++ b/src/Lean/Elab/Notation.lean
@@ -99,8 +99,9 @@ private def expandNotationAux (ref : Syntax)
   | some delabDecl => mkNullNode #[stxDecl, macroDecl, delabDecl]
   | none           => mkNullNode #[stxDecl, macroDecl]
 
-@[builtinMacro Lean.Parser.Command.notation] def expandNotation : Macro
-  | stx@`($attrKind:attrKind notation $[: $prec? ]? $[(name := $name?)]? $[(priority := $prio?)]? $items* => $rhs) => do
+@[builtinMacro Lean.Parser.Command.notation] def expandNotation : Macro := fun stx =>
+  match stx with
+  | `($attrKind:attrKind notation $[: $prec? ]? $[(name := $name?)]? $[(priority := $prio?)]? $items* => $rhs) => do
     -- trigger scoped checks early and only once
     let _ ← toAttributeKind attrKind
     expandNotationAux stx (← Macro.getCurrNamespace) attrKind prec? name? prio? items rhs
diff --git a/src/Lean/Elab/Tactic/BuiltinTactic.lean b/src/Lean/Elab/Tactic/BuiltinTactic.lean
index be8c5c0cdf..a23e15114c 100644
--- a/src/Lean/Elab/Tactic/BuiltinTactic.lean
+++ b/src/Lean/Elab/Tactic/BuiltinTactic.lean
@@ -234,8 +234,9 @@ def renameInaccessibles (mvarId : MVarId) (hs : Array Syntax) : TacticM MVarId :
     assignExprMVar mvarId mvarNew
     return mvarNew.mvarId!
 
-@[builtinTactic «case»] def evalCase : Tactic
-  | stx@`(tactic| case $tag $hs* =>%$arr $tac:tacticSeq) => do
+@[builtinTactic «case»] def evalCase : Tactic := fun stx =>
+  match stx with
+  | `(tactic| case $tag $hs* =>%$arr $tac:tacticSeq) => do
     let gs ← getUnsolvedGoals
     let g ←
       if tag.isIdent then
@@ -258,8 +259,9 @@ def renameInaccessibles (mvarId : MVarId) (hs : Array Syntax) : TacticM MVarId :
     setGoals gs
   | _ => throwUnsupportedSyntax
 
-@[builtinTactic «renameI»] def evalRenameInaccessibles : Tactic
-  | stx@`(tactic| rename_i $hs*) => do replaceMainGoal [← renameInaccessibles (← getMainGoal) hs]
+@[builtinTactic «renameI»] def evalRenameInaccessibles : Tactic := fun stx =>
+  match stx with
+  | `(tactic| rename_i $hs*) => do replaceMainGoal [← renameInaccessibles (← getMainGoal) hs]
   | _ => throwUnsupportedSyntax
 
 @[builtinTactic «first»] partial def evalFirst : Tactic := fun stx => do
diff --git a/src/Lean/Server/FileWorker/RequestHandling.lean b/src/Lean/Server/FileWorker/RequestHandling.lean
index 435d522b5e..4efee2b2f7 100644
--- a/src/Lean/Server/FileWorker/RequestHandling.lean
+++ b/src/Lean/Server/FileWorker/RequestHandling.lean
@@ -219,8 +219,9 @@ partial def handleDocumentHighlight (p : DocumentHighlightParams)
   let doc ← readDoc
   let text := doc.meta.text
   let pos := text.lspPosToUtf8Pos p.position
-  let rec highlightReturn? (doRange? : Option Range) : Syntax → Option DocumentHighlight
-    | stx@`(doElem|return%$i $e) => Id.run <| do
+  let rec highlightReturn? (doRange? : Option Range) : Syntax → Option DocumentHighlight := fun stx =>
+    match stx with
+    | `(doElem|return%$i $e) => Id.run <| do
       if let some range := i.getRange? then
         if range.contains pos then
           return some { range := doRange?.getD (range.toLspRange text), kind? := DocumentHighlightKind.text }