diff --git a/library/logic/examples/colog88.lean b/library/logic/examples/colog88.lean
index f1cc73238c..1532a9ce25 100644
--- a/library/logic/examples/colog88.lean
+++ b/library/logic/examples/colog88.lean
@@ -89,4 +89,4 @@ lemma P0_x0 : P0 x0 :=
 exists.intro P0 (and.intro fP0_eq not_P0_x0)
 
 theorem inconsistent : false :=
-absurd @P0_x0 @not_P0_x0
+absurd P0_x0 not_P0_x0