diff --git a/library/init/meta/interactive.lean b/library/init/meta/interactive.lean
index 093b189b92..587098c5f4 100644
--- a/library/init/meta/interactive.lean
+++ b/library/init/meta/interactive.lean
@@ -11,7 +11,7 @@ import init.meta.lean.parser init.meta.quote
 open lean
 open lean.parser
 
-local postfix ?:9001 := optional
+local postfix `?`:9001 := optional
 local postfix *:9001 := many
 
 namespace interactive
diff --git a/library/init/meta/lean/parser.lean b/library/init/meta/lean/parser.lean
index d18526a29c..b0640d47f8 100644
--- a/library/init/meta/lean/parser.lean
+++ b/library/init/meta/lean/parser.lean
@@ -56,7 +56,7 @@ meta def {u v} many {f : Type u → Type v} [monad f] [alternative f] {a : Type
            ys ← many x,
            return $ y::ys) <|> pure list.nil
 
-local postfix ?:100 := optional
+local postfix `?`:100 := optional
 local postfix * := many
 
 meta def sep_by {α : Type} : string → parser α → parser (list α)
diff --git a/library/init/meta/smt/interactive.lean b/library/init/meta/smt/interactive.lean
index 65177d0d84..58118cc673 100644
--- a/library/init/meta/smt/interactive.lean
+++ b/library/init/meta/smt/interactive.lean
@@ -39,7 +39,7 @@ namespace interactive
 open lean.parser
 open interactive
 open interactive.types
-local postfix ?:9001 := optional
+local postfix `?`:9001 := optional
 local postfix *:9001 := many
 
 meta def itactic : Type :=
diff --git a/src/frontends/lean/notation_cmd.cpp b/src/frontends/lean/notation_cmd.cpp
index a4fee34f84..12bbd00eb9 100644
--- a/src/frontends/lean/notation_cmd.cpp
+++ b/src/frontends/lean/notation_cmd.cpp
@@ -90,7 +90,7 @@ using notation::mk_skip_action;
 using notation::transition;
 using notation::action;
 
-static char const * g_forbidden_tokens[] = {"!", "@", nullptr};
+static char const * g_forbidden_tokens[] = {"@", nullptr};
 
 void check_not_forbidden(char const * tk) {
     auto it = g_forbidden_tokens;
diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp
index ee788fd1f1..9de783f46a 100644
--- a/src/frontends/lean/token_table.cpp
+++ b/src/frontends/lean/token_table.cpp
@@ -88,14 +88,13 @@ void init_token_table(token_table & t) {
          {"[", g_max_prec}, {"]", 0}, {"⦃", g_max_prec}, {"⦄", 0}, {".{", 0},
          {"Type", g_max_prec}, {"Type*", g_max_prec}, {"Sort", g_max_prec}, {"Sort*", g_max_prec},
          {"(:", g_max_prec}, {":)", 0},
-         {"⊢", 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}, {"#", g_max_prec},
+         {"⟨", g_max_prec}, {"⟩", 0}, {"^", 0},
+         {"//", 0}, {"|", 0}, {"with", 0}, {"without", 0}, {"...", 0}, {",", 0},
+         {".", 0}, {":", 0}, {"!", 0}, {"calc", 0}, {"as", 0}, {":=", 0}, {"--", 0}, {"#", g_max_prec},
          {"/-", 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},
-         {"~>", g_max_prec+1},
+         {"match", 0}, {"~>", g_max_prec+1},
          {".1", g_max_prec+1}, {".2", g_max_prec+1}, {".3", g_max_prec+1}, {".4", g_max_prec+1}, {".5", g_max_prec+1}, {".6", g_max_prec+1},
          {".7", g_max_prec+1}, {".8", g_max_prec+1}, {".9", g_max_prec+1},
          {"renaming", 0}, {"extends", 0}, {nullptr, 0}};