diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp
index ad2ef93637..7a1d1c2097 100644
--- a/src/frontends/lean/token_table.cpp
+++ b/src/frontends/lean/token_table.cpp
@@ -96,7 +96,7 @@ void init_token_table(token_table & t) {
          {"/-", 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},
-         {"match", 0}, {"^.", g_max_prec+1},
+         {"match", 0}, {"^.", g_max_prec+1}, {"::", 67},
          {"renaming", 0}, {"extends", 0}, {"node!", g_max_prec}, {"node_choice!", g_max_prec}, {nullptr, 0}};
 
     char const * commands[] =