diff --git a/src/Init/NotationExtra.lean b/src/Init/NotationExtra.lean
index a79ad63bd0..345aeba3fe 100644
--- a/src/Init/NotationExtra.lean
+++ b/src/Init/NotationExtra.lean
@@ -242,6 +242,9 @@ syntax (name := calcTactic) "calc" ppLine withPosition(calcStep) ppLine withPosi
   | `($(_) $a1:str $a2:str $a3:str $a4:str $a5:str $a6:str $a7:str $a8:str) => return mkNode `Lean.Parser.Term.quotedName #[Syntax.mkNameLit s!"`{a1.getString}.{a2.getString}.{a3.getString}.{a4.getString}.{a5.getString}.{a6.getString}.{a7.getString}.{a8.getString}"]
   | _  => throw ()
 
+@[appUnexpander Array.mkArray0] def unexpandMkArray0 : Lean.PrettyPrinter.Unexpander
+  | _ => `(#[])
+
 @[appUnexpander Array.mkArray1] def unexpandMkArray1 : Lean.PrettyPrinter.Unexpander
   | `($(_) $a1) => `(#[$a1])
   | _ => throw ()
diff --git a/tests/lean/ppNotationCode.lean.expected.out b/tests/lean/ppNotationCode.lean.expected.out
index 87a87a0fce..bed5b735cd 100644
--- a/tests/lean/ppNotationCode.lean.expected.out
+++ b/tests/lean/ppNotationCode.lean.expected.out
@@ -67,8 +67,7 @@
                       { raw :=
                             Lean.Syntax.node info `Lean.Parser.Term.app
                               #[Lean.Syntax.node info `term_+++_ #[lhs.raw, Lean.Syntax.atom info "+++", rhs.raw],
-                                Lean.Syntax.node info `null
-                                  (Array.append Array.mkArray0 (Lean.TSyntaxArray.raw moreArgs))] }.raw
+                                Lean.Syntax.node info `null (Array.append #[] (Lean.TSyntaxArray.raw moreArgs))] }.raw
               else
                 let_fun __discr_5 := Lean.Syntax.getArg __discr_2 1;
                 let_fun __discr := Lean.Syntax.getArg __discr 1;