diff --git a/src/Lean/PrettyPrinter/Formatter.lean b/src/Lean/PrettyPrinter/Formatter.lean index 4f6364acef..16fa629397 100644 --- a/src/Lean/PrettyPrinter/Formatter.lean +++ b/src/Lean/PrettyPrinter/Formatter.lean @@ -266,7 +266,7 @@ let id := stx.getId; let s := id.toString; if id.isAnonymous then pushToken "[anonymous]" -else if id.components.any Name.isNum then +else if LocalContext.isInaccessibleUserName id || id.components.any Name.isNum then -- not parsable anyway, output as-is pushToken s else do {