From aafa09ddcd36d021fa1eaab00b5a51073468c205 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 3 Nov 2020 12:30:26 -0800
Subject: [PATCH] chore: fix test

---
 tests/lean/run/newfrontend1.lean | 5 -----
 1 file changed, 5 deletions(-)

diff --git a/tests/lean/run/newfrontend1.lean b/tests/lean/run/newfrontend1.lean
index fd283a75eb..8e093ba641 100644
--- a/tests/lean/run/newfrontend1.lean
+++ b/tests/lean/run/newfrontend1.lean
@@ -136,11 +136,6 @@ by {
 
 macro «try» t:tactic : tactic => `($t <|> skip)
 
-syntax "repeat" tactic : tactic
-macro_rules
-| `(tactic| repeat $t) => `(tactic| try ($t; repeat $t))
-
-
 theorem simple12 (x y z : Nat) : y = z → x = x → x = y → x = z :=
 by {
   intro h1; intro h2; intro h3;