diff --git a/tests/lean/rewrite_loop.lean b/tests/lean/rewrite_loop.lean index cce2d8fbd..945632383 100644 --- a/tests/lean/rewrite_loop.lean +++ b/tests/lean/rewrite_loop.lean @@ -3,5 +3,5 @@ open algebra theorem test {A : Type} [s : comm_ring A] (a b c : A) : a + b + c = a + c + b := begin - rewrite ?add.comm + rewrite *add.comm end