diff --git a/src/Init/Lean/Attributes.lean b/src/Init/Lean/Attributes.lean
index eb758fae12..c328071494 100644
--- a/src/Init/Lean/Attributes.lean
+++ b/src/Init/Lean/Attributes.lean
@@ -53,7 +53,7 @@ IO.mkRef {}
 constant attributeMapRef : IO.Ref (PersistentHashMap Name AttributeImpl) := arbitrary _
 
 /- Low level attribute registration function. -/
-def registerAttribute (attr : AttributeImpl) : IO Unit := do
+def registerBuiltinAttribute (attr : AttributeImpl) : IO Unit := do
 m ← attributeMapRef.get;
 when (m.contains attr.name) $ throw (IO.userError ("invalid attribute declaration, '" ++ toString attr.name ++ "' has already been used"));
 initializing ← IO.initializing;
@@ -185,7 +185,7 @@ let attrImpl : AttributeImpl := {
     | Except.error msg => throw (IO.userError ("invalid attribute '" ++ toString name ++ "', " ++ msg))
     | _                => pure $ ext.addEntry env decl
 };
-registerAttribute attrImpl;
+registerBuiltinAttribute attrImpl;
 pure { attr := attrImpl, ext := ext }
 
 namespace TagAttribute
@@ -237,7 +237,7 @@ let attrImpl : AttributeImpl := {
       | Except.error msg => throw (IO.userError ("invalid attribute '" ++ toString name ++ "', " ++ msg))
       | Except.ok env    => pure env
 };
-registerAttribute attrImpl;
+registerBuiltinAttribute attrImpl;
 pure { attr := attrImpl, ext := ext }
 
 namespace ParametricAttribute
@@ -293,7 +293,7 @@ let attrs := attrDescrs.map $ fun ⟨name, descr, val⟩ => { AttributeImpl .
     | Except.error msg => throw (IO.userError ("invalid attribute '" ++ toString name ++ "', " ++ msg))
     | _                => pure $ ext.addEntry env (decl, val)
 };
-attrs.forM registerAttribute;
+attrs.forM registerBuiltinAttribute;
 pure { ext := ext, attrs := attrs }
 
 namespace EnumAttributes
diff --git a/src/Init/Lean/Class.lean b/src/Init/Lean/Class.lean
index ab7015cc96..a7e5d0aa7c 100644
--- a/src/Init/Lean/Class.lean
+++ b/src/Init/Lean/Class.lean
@@ -137,7 +137,7 @@ partial def getClassName (env : Environment) : Expr → Option Name
     else none
 
 @[init] def registerClassAttr : IO Unit :=
-registerAttribute {
+registerBuiltinAttribute {
   name  := `class,
   descr := "type class",
   add   := fun env decl args persistent => do
diff --git a/src/Init/Lean/Elab/Command.lean b/src/Init/Lean/Elab/Command.lean
index 36160b2bdf..aac26fdbbd 100644
--- a/src/Init/Lean/Elab/Command.lean
+++ b/src/Init/Lean/Elab/Command.lean
@@ -159,7 +159,7 @@ match env.addAndCompile {} decl with
 | Except.ok env  => IO.ofExcept (setInitAttr env name)
 
 @[init] def registerBuiltinCommandElabAttr : IO Unit :=
-registerAttribute {
+registerBuiltinAttribute {
  name  := `builtinCommandElab,
  descr := "Builtin command elaborator",
  add   := fun env declName arg persistent => do {
diff --git a/src/Init/Lean/Elab/Term.lean b/src/Init/Lean/Elab/Term.lean
index c34aa18c84..f7bedb3e78 100644
--- a/src/Init/Lean/Elab/Term.lean
+++ b/src/Init/Lean/Elab/Term.lean
@@ -189,7 +189,7 @@ match env.addAndCompile {} decl with
 | Except.ok env  => IO.ofExcept (setInitAttr env name)
 
 @[init] def registerBuiltinTermElabAttr : IO Unit :=
-registerAttribute {
+registerBuiltinAttribute {
  name  := `builtinTermElab,
  descr := "Builtin term elaborator",
  add   := fun env declName arg persistent => do {
diff --git a/src/Init/Lean/Elab/Util.lean b/src/Init/Lean/Elab/Util.lean
index 910238afa6..f66e26f8b8 100644
--- a/src/Init/Lean/Elab/Util.lean
+++ b/src/Init/Lean/Elab/Util.lean
@@ -121,7 +121,7 @@ let attrImpl : AttributeImpl := {
   add             := ElabAttribute.add parserNamespace typeName ext,
   applicationTime := AttributeApplicationTime.afterCompilation
 };
-registerAttribute attrImpl;
+registerBuiltinAttribute attrImpl;
 pure { ext := ext, attr := attrImpl, kind := kind }
 
 @[init] private def regTraceClasses : IO Unit := do
diff --git a/src/Init/Lean/Meta/Instances.lean b/src/Init/Lean/Meta/Instances.lean
index 4abaaf5dac..8ff4fa7df4 100644
--- a/src/Init/Lean/Meta/Instances.lean
+++ b/src/Init/Lean/Meta/Instances.lean
@@ -44,7 +44,7 @@ match env.find? constName with
   pure $ instanceExtension.addEntry env { keys := keys, val := c }
 
 @[init] def registerInstanceAttr : IO Unit :=
-registerAttribute {
+registerBuiltinAttribute {
   name  := `instance,
   descr := "type class instance",
   add   := fun env declName args persistent => do
diff --git a/src/Init/Lean/Parser/Parser.lean b/src/Init/Lean/Parser/Parser.lean
index bd8bb126c0..bb85f4acd4 100644
--- a/src/Init/Lean/Parser/Parser.lean
+++ b/src/Init/Lean/Parser/Parser.lean
@@ -1640,7 +1640,7 @@ The parsing tables for builtin parsers are "stored" in the extracted source code
 -/
 def registerBuiltinParserAttribute (attrName : Name) (catName : Name) : IO Unit := do
 addBuiltinParserCategory catName;
-registerAttribute {
+registerBuiltinAttribute {
  name            := attrName,
  descr           := "Builtin parser",
  add             := BuiltinParserAttribute.add attrName catName,
@@ -1681,7 +1681,7 @@ let attrImpl : AttributeImpl := {
   add             := ParserAttribute.add attrName catName,
   applicationTime := AttributeApplicationTime.afterCompilation
 };
-registerAttribute attrImpl
+registerBuiltinAttribute attrImpl -- TODO improve
 
 -- declare `termParser` here since it is used everywhere via antiquotations