diff --git a/src/Init/Data/Repr.lean b/src/Init/Data/Repr.lean
index 118c3f4851..a38a7e1990 100644
--- a/src/Init/Data/Repr.lean
+++ b/src/Init/Data/Repr.lean
@@ -93,6 +93,32 @@ toDigitsCore base (n+1) n []
 protected def repr (n : Nat) : String :=
 (toDigits 10 n).asString
 
+def superDigitChar (n : Nat) : Char :=
+if n = 0 then '⁰' else
+if n = 1 then '¹' else
+if n = 2 then '²' else
+if n = 3 then '³' else
+if n = 4 then '⁴' else
+if n = 5 then '⁵' else
+if n = 6 then '⁶' else
+if n = 7 then '⁷' else
+if n = 8 then '⁸' else
+if n = 9 then '⁹' else
+'*'
+
+partial def toSuperDigitsAux : Nat → List Char → List Char
+| n, ds =>
+  let d  := superDigitChar $ n % 10;
+  let n' := n / 10;
+  if n' = 0 then d::ds
+  else toSuperDigitsAux n' (d::ds)
+
+def toSuperDigits (n : Nat) : List Char :=
+toSuperDigitsAux n []
+
+def toSuperscriptString (n : Nat) : String :=
+(toSuperDigits n).asString
+
 end Nat
 
 instance : HasRepr Nat :=
diff --git a/src/Lean/LocalContext.lean b/src/Lean/LocalContext.lean
index c3648a23bd..3d1bbdbb8e 100644
--- a/src/Lean/LocalContext.lean
+++ b/src/Lean/LocalContext.lean
@@ -371,30 +371,62 @@ Id.run $ lctx.anyM p
 @[inline] def all (lctx : LocalContext) (p : LocalDecl → Bool) : Bool :=
 Id.run $ lctx.allM p
 
-partial def renameShadowedUserName (usedNames : NameMap Nat) (userName : Name) : Nat → Name × NameMap Nat
-| i =>
-  let userNameNew := mkNameNum (mkNameStr userName "_shadowed") i;
-  if usedNames.contains userNameNew then
-    renameShadowedUserName (i+1)
-  else
-    (userNameNew, usedNames.insert userName (i+1))
+private def mkInaccessibleUserNameAux (unicode : Bool) (name : Name) (idx : Nat) : Name :=
+if unicode then
+  name.appendAfter ("✝" ++ idx.toSuperscriptString)
+else
+  name ++ mkNameNum "_inaccessible" idx
 
-def sanitizeNames (lctx : LocalContext) : LocalContext :=
-Prod.fst $ lctx.decls.size.foldRev
+private def mkInaccessibleUserName (unicode : Bool) : Name → Name
+| Name.num p@(Name.str _ _ _) idx _ =>
+  mkInaccessibleUserNameAux unicode p idx
+| Name.num Name.anonymous idx _     =>
+  mkInaccessibleUserNameAux unicode Name.anonymous idx
+| Name.num p idx _ =>
+  if unicode then
+    (mkInaccessibleUserName p).appendAfter ("⁻" ++ idx.toSuperscriptString)
+  else
+    mkNameNum (mkInaccessibleUserName p) idx
+| n => n
+
+@[export lean_is_inaccessible_user_name]
+def isInaccessibleUserName : Name → Bool
+| Name.str _ s _   => s.contains '✝' || s == "_inaccessible"
+| Name.num p idx _ => isInaccessibleUserName p
+| _                => false
+
+private def sanitizeMacroScopes (unicode : Bool) (mainModule : Name) (userName : Name) : Name :=
+if !userName.hasMacroScopes then
+  userName
+else
+  let userName := if (extractMacroScopes userName).mainModule == mainModule then userName.simpMacroScopes else userName;
+  mkInaccessibleUserName unicode userName
+
+private partial def mkFreshInaccessibleUserName (unicode : Bool) (usedName2Idx : NameMap Nat) (userName : Name) : Nat → Name × NameMap Nat
+| idx =>
+  let userNameNew := mkInaccessibleUserName unicode (mkNameNum userName idx);
+  if usedName2Idx.contains userNameNew then
+    mkFreshInaccessibleUserName (idx+1)
+  else
+   (userNameNew, usedName2Idx.insert userName (idx+1))
+
+def sanitizeNames (lctx : LocalContext) (options : Options) (mainModule : Name) : LocalContext :=
+let unicode   := Format.getUnicode options;
+let (lctx, _) := lctx.decls.size.foldRev
   (fun i (acc : LocalContext × NameMap Nat) =>
-    let (lctx, usedNames) := acc;
+    let (lctx, usedName2Idx) := acc;
     match lctx.decls.get! i with
     | none      => acc
-    | some decl =>
-      let userName := decl.userName;
-      if userName.hasMacroScopes then acc
-      else match usedNames.find? userName with
-      | none     => (lctx, usedNames.insert userName 1)
+    | some decl => do
+      let userName := decl.userName.eraseMacroScopes;
+      match usedName2Idx.find? userName with
+      | none     => (lctx, usedName2Idx.insert userName 1)
       | some idx =>
-        let (userNameNew, usedNames) := renameShadowedUserName usedNames userName idx;
+        let (userNameNew, usedName2Idx) := mkFreshInaccessibleUserName unicode usedName2Idx userName idx;
         let lctx := lctx.setUserName decl.fvarId userNameNew;
-        (lctx, usedNames))
-  (lctx, {})
+        (lctx, usedName2Idx))
+  (lctx, {});
+lctx
 
 end LocalContext
 
diff --git a/src/Lean/Message.lean b/src/Lean/Message.lean
index 82b76c4aa2..71ea3ff1d7 100644
--- a/src/Lean/Message.lean
+++ b/src/Lean/Message.lean
@@ -65,7 +65,7 @@ def getSanitizeNames (o : Options) : Bool:= o.get `pp.sanitizeNames sanitizeName
 
 private def sanitizeNames (ctx : MessageDataContext) : MessageDataContext :=
 if getSanitizeNames ctx.opts then
-  { ctx with lctx := ctx.lctx.sanitizeNames }
+  { ctx with lctx := ctx.lctx.sanitizeNames ctx.opts ctx.env.mainModule }
 else
   ctx