diff --git a/Std/Data/Array/Lemmas.lean b/Std/Data/Array/Lemmas.lean
index 421589709b..f6a82f2e47 100644
--- a/Std/Data/Array/Lemmas.lean
+++ b/Std/Data/Array/Lemmas.lean
@@ -5,7 +5,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Gabriel Ebner
 -/
 import Std.Data.List.Lemmas
-import Std.Data.Array.Init.Lemmas
 import Std.Data.Array.Basic
 import Std.Tactic.SeqFocus
 import Std.Util.ProofWanted
diff --git a/Std/Data/Array/Merge.lean b/Std/Data/Array/Merge.lean
index 2c71ea6eaf..250ab760e1 100644
--- a/Std/Data/Array/Merge.lean
+++ b/Std/Data/Array/Merge.lean
@@ -3,6 +3,7 @@ Copyright (c) 2022 Jannis Limperg. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jannis Limperg
 -/
+import Std.Tactic.Alias
 
 namespace Array
 
diff --git a/Std/Tactic/PrintPrefix.lean b/Std/Tactic/PrintPrefix.lean
index ca757c8e15..b342b38b12 100644
--- a/Std/Tactic/PrintPrefix.lean
+++ b/Std/Tactic/PrintPrefix.lean
@@ -73,12 +73,11 @@ private def lexNameLt : Name -> Name -> Bool
 | .str _ _, .num _ _ => false
 | .str p m, .str q n => m < n || m == n && lexNameLt p q
 
-private def appendMatchingConstants (msg : MessageData) (opts : PrintPrefixConfig) (pre : Name)
-     : MetaM MessageData := do
+private def matchingConstants (opts : PrintPrefixConfig) (pre : Name)
+     : MetaM (Array MessageData) := do
   let cinfos ← getMatchingConstants (matchName opts pre) opts.imported
   let cinfos := cinfos.qsort fun p q => lexNameLt (reverseName p.name) (reverseName q.name)
-  let mut msg := msg
-  let ppInfo cinfo : MetaM MessageData := do
+  cinfos.mapM fun cinfo => do
     if opts.showTypes then
       pure <| .ofPPFormat { pp := fun
         | some ctx => ctx.runMetaM <|
@@ -87,9 +86,6 @@ private def appendMatchingConstants (msg : MessageData) (opts : PrintPrefixConfi
       } ++ "\n"
     else
       pure m!"{ppConst (← mkConstWithLevelParams cinfo.name)}\n"
-  for cinfo in cinfos do
-    msg := msg ++ (← ppInfo cinfo)
-  pure msg
 
 /--
 The command `#print prefix foo` will print all definitions that start with
@@ -122,9 +118,8 @@ elab (name := printPrefix) "#print" tk:"prefix"
     cfg:(Lean.Parser.Tactic.config)? name:ident : command => liftTermElabM do
   let nameId := name.getId
   let opts ← elabPrintPrefixConfig (mkOptionalNode cfg)
-  let mut msg ← appendMatchingConstants "" opts nameId
-  if msg.isEmpty then
+  let mut msgs ← matchingConstants opts nameId
+  if msgs.isEmpty then
     if let [name] ← resolveGlobalConst name then
-      msg ← appendMatchingConstants msg opts name
-  if !msg.isEmpty then
-    logInfoAt tk msg
+      msgs ← matchingConstants opts name
+  logInfoAt tk (.joinSep msgs.toList "")
diff --git a/test/print_prefix.lean b/test/print_prefix.lean
index 625ba47b2e..6677469882 100644
--- a/test/print_prefix.lean
+++ b/test/print_prefix.lean
@@ -12,6 +12,7 @@ TEmpty.recOn.{u} (motive : TEmpty → Sort u) (t : TEmpty) : motive t
 #guard_msgs in
 #print prefix TEmpty -- Test type that probably won't change much.
 
+/-- info: -/
 #guard_msgs in
 #print prefix (config := {imported := false}) Empty