diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp
index 8dbda875b3..9c246a7dba 100644
--- a/src/frontends/lean/token_table.cpp
+++ b/src/frontends/lean/token_table.cpp
@@ -89,7 +89,7 @@ void init_token_table(token_table & t) {
          {"⊢", 0}, {"⟨", g_max_prec}, {"⟩", 0}, {"^", 0}, {"↑", 0}, {"▸", 0},
          {"//", 0}, {"|", 0}, {"!", g_max_prec}, {"?", 0},  {"with", 0}, {"without", 0}, {"...", 0}, {",", 0},
          {".", 0}, {":", 0}, {"::", 0}, {"calc", 0}, {"as", 0}, {":=", 0}, {"--", 0}, {"#", 0},
-         {"(*", 0}, {"/-", 0}, {"begin", g_max_prec}, {"abstract", g_max_prec}, {"using", 0},
+         {"(*", 0}, {"/-", 0}, {"begin", g_max_prec}, {"using", 0},
          {"@@", g_max_prec}, {"@", g_max_prec},
          {"sorry", g_max_prec}, {"+", g_plus_prec}, {"->", g_arrow_prec}, {"<-", 0},
          {"?(", g_max_prec}, {"⌞", g_max_prec}, {"⌟", 0}, {"match", 0},