diff --git a/library/init/core.lean b/library/init/core.lean
index 80831246fc..56f8b0d924 100644
--- a/library/init/core.lean
+++ b/library/init/core.lean
@@ -1395,8 +1395,7 @@ end plift
 class inhabited (α : Sort u) :=
 (default : α)
 
--- TODO: mark as opaque
-def default (α : Sort u) [inhabited α] : α :=
+constant default (α : Sort u) [inhabited α] : α :=
 inhabited.default α
 
 @[inline, irreducible] def arbitrary (α : Sort u) [inhabited α] : α :=