diff --git a/src/Init/Conv.lean b/src/Init/Conv.lean
index 149c4e7c7a..f974028bc0 100644
--- a/src/Init/Conv.lean
+++ b/src/Init/Conv.lean
@@ -286,7 +286,7 @@ macro:1 x:conv tk:" <;> " y:conv:0 : conv =>
 /-- `repeat convs` runs the sequence `convs` repeatedly until it fails to apply. -/
 syntax "repeat " convSeq : conv
 macro_rules
-  | `(conv| repeat $seq) => `(conv| first | ($seq); repeat $seq | rfl)
+  | `(conv| repeat $seq) => `(conv| first | ($seq); repeat $seq | skip)
 
 /--
 `conv => ...` allows the user to perform targeted rewriting on a goal or hypothesis,