diff --git a/src/Lean/Linter/Basic.lean b/src/Lean/Linter/Basic.lean
index 5f413ff8d4..7c2686bb42 100644
--- a/src/Lean/Linter/Basic.lean
+++ b/src/Lean/Linter/Basic.lean
@@ -124,7 +124,7 @@ def unusedVariables : Linter := fun stx => do
   return ()
 where
   skipDeclIdIfPresent (stx : Syntax) : Syntax :=
-    if stx.isOfKind `Lean.Parser.Command.declId then
+    if stx.isOfKind ``Lean.Parser.Command.declId then
       stx[0]
     else
       stx
@@ -133,69 +133,69 @@ where
     let some declRange := stx.getRange?
       | false
     constDecls.contains declRange &&
-    !stackMatches stack [`Lean.Parser.Term.letIdDecl]
+    !stackMatches stack [``Lean.Parser.Term.letIdDecl]
   matchesUnusedPattern (stx : Syntax) (_ : SyntaxStack) :=
     stx.getId.toString.startsWith "_"
   isVariable (_ : Syntax) (stack : SyntaxStack) :=
-    stackMatches stack [`null, none, `null, `Lean.Parser.Command.variable]
+    stackMatches stack [`null, none, `null, ``Lean.Parser.Command.variable]
   isInStructure (_ : Syntax) (stack : SyntaxStack) :=
-    stackMatches stack [`null, none, `null, `Lean.Parser.Command.structure]
+    stackMatches stack [`null, none, `null, ``Lean.Parser.Command.structure]
   isInInductive (_ : Syntax) (stack : SyntaxStack) :=
-    stackMatches stack [`null, none, `null, none, `Lean.Parser.Command.inductive] &&
+    stackMatches stack [`null, none, `null, none, ``Lean.Parser.Command.inductive] &&
     (stack.get? 3 |>.any fun (stx, pos) =>
       pos == 0 &&
-      [`Lean.Parser.Command.optDeclSig, `Lean.Parser.Command.declSig].any (stx.isOfKind ·))
+      [``Lean.Parser.Command.optDeclSig, ``Lean.Parser.Command.declSig].any (stx.isOfKind ·))
   isInCtorOrStructBinder (_ : Syntax) (stack : SyntaxStack) :=
-    stackMatches stack [`null, none, `null, `Lean.Parser.Command.optDeclSig, none] &&
+    stackMatches stack [`null, none, `null, ``Lean.Parser.Command.optDeclSig, none] &&
     (stack.get? 4 |>.any fun (stx, _) =>
-      [`Lean.Parser.Command.ctor, `Lean.Parser.Command.structSimpleBinder].any (stx.isOfKind ·))
+      [``Lean.Parser.Command.ctor, ``Lean.Parser.Command.structSimpleBinder].any (stx.isOfKind ·))
   isInConstantOrAxiom (_ : Syntax) (stack : SyntaxStack) :=
-    stackMatches stack [`null, none, `null, `Lean.Parser.Command.declSig, none] &&
+    stackMatches stack [`null, none, `null, ``Lean.Parser.Command.declSig, none] &&
     (stack.get? 4 |>.any fun (stx, _) =>
-      [`Lean.Parser.Command.constant, `Lean.Parser.Command.axiom].any (stx.isOfKind ·))
+      [``Lean.Parser.Command.constant, ``Lean.Parser.Command.axiom].any (stx.isOfKind ·))
   isInDefWithForeignDefinition (_ : Syntax) (stack : SyntaxStack) :=
-    stackMatches stack [`null, none, `null, none, none, `Lean.Parser.Command.declaration] &&
+    stackMatches stack [`null, none, `null, none, none, ``Lean.Parser.Command.declaration] &&
     (stack.get? 3 |>.any fun (stx, _) =>
-      stx.isOfKind `Lean.Parser.Command.optDeclSig ||
-      stx.isOfKind `Lean.Parser.Command.declSig) &&
+      stx.isOfKind ``Lean.Parser.Command.optDeclSig ||
+      stx.isOfKind ``Lean.Parser.Command.declSig) &&
     (stack.get? 5 |>.any fun (stx, _) => Id.run <| do
       let declModifiers := stx[0]
-      if !declModifiers.isOfKind `Lean.Parser.Command.declModifiers then
+      if !declModifiers.isOfKind ``Lean.Parser.Command.declModifiers then
         return false
       let termAttributes := declModifiers[1][0]
-      if !termAttributes.isOfKind `Lean.Parser.Term.attributes then
+      if !termAttributes.isOfKind ``Lean.Parser.Term.attributes then
         return false
       let termAttrInstance := termAttributes[1][0]
-      if !termAttrInstance.isOfKind `Lean.Parser.Term.attrInstance then
+      if !termAttrInstance.isOfKind ``Lean.Parser.Term.attrInstance then
         return false
 
       let attr := termAttrInstance[1]
-      if attr.isOfKind `Lean.Parser.Attr.extern then
+      if attr.isOfKind ``Lean.Parser.Attr.extern then
         return true
-      else if attr.isOfKind `Lean.Parser.Attr.simple then
+      else if attr.isOfKind ``Lean.Parser.Attr.simple then
         return attr[0].getId == `implementedBy
       else
         return false)
   isInDepArrow (_ : Syntax) (stack : SyntaxStack) :=
-    stackMatches stack [`null, `Lean.Parser.Term.explicitBinder, `Lean.Parser.Term.depArrow]
+    stackMatches stack [`null, ``Lean.Parser.Term.explicitBinder, ``Lean.Parser.Term.depArrow]
 
   isInLetDeclaration (_ : Syntax) (stack : SyntaxStack) :=
-    stackMatches stack [`null, none, `null, `Lean.Parser.Term.letIdDecl, none] &&
+    stackMatches stack [`null, none, `null, ``Lean.Parser.Term.letIdDecl, none] &&
     (stack.get? 3 |>.any fun (_, pos) => pos == 1) &&
-    (stack.get? 5 |>.any fun (stx, _) => !stx.isOfKind `Lean.Parser.Command.whereStructField)
+    (stack.get? 5 |>.any fun (stx, _) => !stx.isOfKind ``Lean.Parser.Command.whereStructField)
   isInDeclarationSignature (_ : Syntax) (stack : SyntaxStack) :=
     stackMatches stack [`null, none, `null, none] &&
     (stack.get? 3 |>.any fun (stx, pos) =>
       pos == 0 &&
-      [`Lean.Parser.Command.optDeclSig, `Lean.Parser.Command.declSig].any (stx.isOfKind ·))
+      [``Lean.Parser.Command.optDeclSig, ``Lean.Parser.Command.declSig].any (stx.isOfKind ·))
   isInFun (_ : Syntax) (stack : SyntaxStack) :=
-    stackMatches stack [`null, `Lean.Parser.Term.basicFun] ||
-    stackMatches stack [`null, `Lean.Parser.Term.paren, `null, `Lean.Parser.Term.basicFun]
+    stackMatches stack [`null, ``Lean.Parser.Term.basicFun] ||
+    stackMatches stack [`null, ``Lean.Parser.Term.paren, `null, ``Lean.Parser.Term.basicFun]
 
   isPatternVar (_ : Syntax) (stack : SyntaxStack) :=
     stack.any fun (stx, pos) =>
-      (stx.isOfKind `Lean.Parser.Term.matchAlt && pos == 1) ||
-      (stx.isOfKind `Lean.Parser.Tactic.inductionAlt && pos == 2)
+      (stx.isOfKind ``Lean.Parser.Term.matchAlt && pos == 1) ||
+      (stx.isOfKind ``Lean.Parser.Tactic.inductionAlt && pos == 2)
 
 builtin_initialize addLinter unusedVariables