diff --git a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
index 3d71f1b4be..1e75bac785 100644
--- a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
@@ -219,7 +219,7 @@ def delabAppMatch : Delab := whenPPOption getPPNotation do
     Syntax.mkApp stx st.moreArgs
   | _,        #[] => failure
   | _,        _   =>
-    let discrs ← st.discrs.mapM fun discr => `(Parser.Term.matchDiscr|$discr:term)
+    let discrs ← st.discrs.mapM fun discr => `(matchDiscr|$discr:term)
     let pats ← delabPatterns st
     let stx ← `(match $[$discrs],* with | $[$[$pats],* => $st.rhss]|*)
     Syntax.mkApp stx st.moreArgs