diff --git a/src/Init/Lean/Parser/Parser.lean b/src/Init/Lean/Parser/Parser.lean index 8735fb1dc6..1d8618e5a9 100644 --- a/src/Init/Lean/Parser/Parser.lean +++ b/src/Init/Lean/Parser/Parser.lean @@ -1767,7 +1767,10 @@ private def catNameToString : Name → String | n => n.toString def categoryParserFnImpl (catName : Name) : ParserFn leading := -orelseFn (mkAntiquot (catNameToString catName) none false).fn (categoryParserFnImplAux catName) +if catName != `term then + orelseFn (mkAntiquot (catNameToString catName) none false).fn (categoryParserFnImplAux catName) +else + categoryParserFnImplAux catName @[init] def setCategoryParserFnRef : IO Unit := categoryParserFnRef.set categoryParserFnImpl