diff --git a/library/standard/unit.lean b/library/standard/unit.lean
index 4bdefb1b6..46ecfc63f 100644
--- a/library/standard/unit.lean
+++ b/library/standard/unit.lean
@@ -6,13 +6,15 @@ using decidable
 
 namespace unit
 inductive unit : Type :=
-| tt : unit
+| star : unit
+
+notation `⋆`:max := star
 
 theorem unit_eq (a b : unit) : a = b
-:= unit_rec (unit_rec (refl tt) b) a
+:= unit_rec (unit_rec (refl ⋆) b) a
 
 theorem inhabited_unit [instance] : inhabited unit
-:= inhabited_intro tt
+:= inhabited_intro ⋆
 
 using decidable
 theorem decidable_eq [instance] (a b : unit) : decidable (a = b)