diff --git a/src/Init/Meta.lean b/src/Init/Meta.lean
index a5602fd505..8d5b23c0d2 100644
--- a/src/Init/Meta.lean
+++ b/src/Init/Meta.lean
@@ -792,7 +792,7 @@ instance : Quote Substring := ⟨fun s => Syntax.mkCApp `String.toSubstring #[qu
 
 -- in contrast to `Name.toString`, we can, and want to be, precise here
 private def getEscapedNameParts? (acc : List String) : Name → Option (List String)
-  | Name.anonymous => return acc
+  | Name.anonymous => if acc.isEmpty then none else some acc
   | Name.str n s _ => do
     let s ← Name.escapePart s
     getEscapedNameParts? (s::acc) n