From 830606757b47801a6d512f6b099ddd8dace91f3d Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 20 May 2019 10:23:50 -0700
Subject: [PATCH] fix(library/init/lean/name_mangling): make sure name mangling
 procedure behaves like the C++ one

---
 library/init/lean/name_mangling.lean | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/library/init/lean/name_mangling.lean b/library/init/lean/name_mangling.lean
index e74c9b809c..c0253b7bab 100644
--- a/library/init/lean/name_mangling.lean
+++ b/library/init/lean/name_mangling.lean
@@ -40,9 +40,10 @@ String.mangleAux s.length s.mkIterator ""
 private def Name.mangleAux (pre : String) : Name → String
 | Name.anonymous       := pre
 | (Name.mkString p s) :=
-  let r := Name.mangleAux p in
   let m := String.mangle s in
-  r ++ "_s" ++ toString m.length ++ "_" ++ m
+  match p with
+  | Name.anonymous := m
+  | _              := (Name.mangleAux p) ++ "_" ++ m
 | (Name.mkNumeral p n) :=
   let r := Name.mangleAux p in
   r ++ "_" ++ toString n ++ "_"