diff --git a/src/builtin/kernel.lean b/src/builtin/kernel.lean
index c31b0d6ac..d03d36809 100644
--- a/src/builtin/kernel.lean
+++ b/src/builtin/kernel.lean
@@ -49,7 +49,6 @@ infix 50 ≠ : neq
 theorem em (a : Bool) : a ∨ ¬ a
 := λ Hna : ¬ a, Hna
 
--- Boolean completeness
 axiom case (P : Bool → Bool) (H1 : P true) (H2 : P false) (a : Bool) : P a
 
 axiom refl {A : TypeU} (a : A) : a == a