diff --git a/src/Lean/Parser/Parser.lean b/src/Lean/Parser/Parser.lean index b50cb62890..b65aacc256 100644 --- a/src/Lean/Parser/Parser.lean +++ b/src/Lean/Parser/Parser.lean @@ -1862,12 +1862,8 @@ match (parserExtension.getState env).categories.find? catName with | none => false | some cat => cat.leadingIdentAsSymbol -private def catNameToString : Name → String -| Name.str Name.anonymous s _ => s -| n => n.toString - -@[inline] def mkCategoryAntiquotParser (kind : Name) : Parser := -mkAntiquot (catNameToString kind) none +def mkCategoryAntiquotParser (kind : Name) : Parser := +mkAntiquot kind.toString none def categoryParserFnImpl (catName : Name) : ParserFn := fun ctx s =>