diff --git a/hott/algebra/binary.hlean b/hott/algebra/binary.hlean
index bdf676e5ef..2c9f3d93fd 100644
--- a/hott/algebra/binary.hlean
+++ b/hott/algebra/binary.hlean
@@ -15,9 +15,9 @@ namespace binary
     variable {A : Type}
     variables (op₁ : A → A → A) (inv : A → A) (one : A)
 
-    notation [local] a * b := op₁ a b
-    notation [local] a ⁻¹  := inv a
-    notation [local] 1     := one
+    local notation a * b := op₁ a b
+    local notation a ⁻¹  := inv a
+    local notation 1     := one
 
     definition commutative := ∀a b, a*b = b*a
     definition associative := ∀a b c, (a*b)*c = a*(b*c)
@@ -35,7 +35,7 @@ namespace binary
 
     variable (op₂ : A → A → A)
 
-    notation [local] a + b := op₂ a b
+    local notation a + b := op₂ a b
 
     definition left_distributive := ∀a b c, a * (b + c) = a * b + a * c
     definition right_distributive := ∀a b c, (a + b) * c = a * c + b * c
diff --git a/hott/init/relation.hlean b/hott/init/relation.hlean
index 91e3154824..ef673bcd5e 100644
--- a/hott/init/relation.hlean
+++ b/hott/init/relation.hlean
@@ -10,7 +10,7 @@ import init.logic
 -- We need some of the following definitions asap when "initializing" Lean.
 
 variables {A B : Type} (R : B → B → Type)
-infix [local] `≺`:50 := R
+local infix `≺`:50 := R
 
 definition reflexive := ∀x, x ≺ x
 
diff --git a/hott/types/sigma.hlean b/hott/types/sigma.hlean
index d1f462d6e1..6069222429 100644
--- a/hott/types/sigma.hlean
+++ b/hott/types/sigma.hlean
@@ -11,7 +11,7 @@ import types.prod
 open eq sigma sigma.ops equiv is_equiv
 
 namespace sigma
-  infixr [local] ∘ := function.compose --remove
+  local infixr ∘ := function.compose --remove
   variables {A A' : Type} {B : A → Type} {B' : A' → Type} {C : Πa, B a → Type}
             {D : Πa b, C a b → Type}
             {a a' a'' : A} {b b₁ b₂ : B a} {b' : B a'} {b'' : B a''} {u v w : Σa, B a}
diff --git a/library/algebra/binary.lean b/library/algebra/binary.lean
index 8dcca16651..060a8cb0a7 100644
--- a/library/algebra/binary.lean
+++ b/library/algebra/binary.lean
@@ -16,9 +16,9 @@ namespace binary
     variable {A : Type}
     variables (op₁ : A → A → A) (inv : A → A) (one : A)
 
-    notation [local] a * b := op₁ a b
-    notation [local] a ⁻¹  := inv a
-    notation [local] 1     := one
+    local notation a * b := op₁ a b
+    local notation a ⁻¹  := inv a
+    local notation 1     := one
 
     definition commutative := ∀a b, a * b = b * a
     definition associative := ∀a b c, (a * b) * c = a * (b * c)
@@ -36,7 +36,7 @@ namespace binary
 
     variable (op₂ : A → A → A)
 
-    notation [local] a + b := op₂ a b
+    local notation a + b := op₂ a b
 
     definition left_distributive := ∀a b c, a * (b + c) = a * b + a * c
     definition right_distributive := ∀a b c, (a + b) * c = a * c + b * c
diff --git a/library/data/int/basic.lean b/library/data/int/basic.lean
index b2590cb298..82949d22e3 100644
--- a/library/data/int/basic.lean
+++ b/library/data/int/basic.lean
@@ -151,7 +151,7 @@ cases_on a
 
 definition equiv (p q : ℕ × ℕ) : Prop :=  pr1 p + pr2 q = pr2 p + pr1 q
 
-notation [local] p `≡` q := equiv p q
+local notation p `≡` q := equiv p q
 
 theorem equiv.refl {p : ℕ × ℕ} : p ≡ p := !add.comm
 
diff --git a/library/data/nat/div.lean b/library/data/nat/div.lean
index fc9a086685..9d8fbc300a 100644
--- a/library/data/nat/div.lean
+++ b/library/data/nat/div.lean
@@ -334,7 +334,7 @@ private definition pair_nat.lt.wf : well_founded pair_nat.lt :=
 intro_k (measure.wf pr₂) 20  -- we use intro_k to be able to execute gcd efficiently in the kernel
 
 local attribute pair_nat.lt.wf [instance]      -- instance will not be saved in .olean
-infixl [local] `≺`:50 := pair_nat.lt
+local infixl `≺`:50 := pair_nat.lt
 
 private definition gcd.lt.dec (x y₁ : nat) : (succ y₁, x mod succ y₁) ≺ (x, succ y₁) :=
 mod_lt (succ_pos y₁)
diff --git a/library/init/relation.lean b/library/init/relation.lean
index 059c361aad..0477ab3300 100644
--- a/library/init/relation.lean
+++ b/library/init/relation.lean
@@ -12,7 +12,7 @@ import init.logic
 -- We need some of the following definitions asap when "initializing" Lean.
 
 variables {A B : Type} (R : B → B → Prop)
-infix [local] `≺`:50 := R
+local infix `≺`:50 := R
 
 definition reflexive := ∀x, x ≺ x
 
diff --git a/src/emacs/lean-syntax.el b/src/emacs/lean-syntax.el
index 73e3037169..331bb62e8e 100644
--- a/src/emacs/lean-syntax.el
+++ b/src/emacs/lean-syntax.el
@@ -118,7 +118,7 @@
      ;; modifiers
      (,(rx (or "\[persistent\]" "\[notation\]" "\[visible\]" "\[instance\]" "\[class\]" "\[parsing-only\]"
                "\[coercion\]" "\[reducible\]" "\[irreducible\]" "\[wf\]" "\[whnf\]" "\[multiple-instances\]"
-               "\[decls\]" "\[strict\]" "\[local\]" "\[coercions\]" "\[classes\]" "\[notations\]" "\[tactic_hints\]" "\[reduce_hints\]"))
+               "\[decls\]" "\[strict\]" "\[coercions\]" "\[classes\]" "\[notations\]" "\[tactic_hints\]" "\[reduce_hints\]"))
       . 'font-lock-doc-face)
      (,(rx "\[priority" (zero-or-more (not (any "\]"))) "\]") . font-lock-doc-face)
      ;; tactics
diff --git a/src/frontends/lean/notation_cmd.cpp b/src/frontends/lean/notation_cmd.cpp
index 35cc9d2227..041e302131 100644
--- a/src/frontends/lean/notation_cmd.cpp
+++ b/src/frontends/lean/notation_cmd.cpp
@@ -610,15 +610,11 @@ static environment add_user_token(environment const & env, char const * val, uns
 }
 
 struct notation_modifiers {
-    bool m_persistent;
     bool m_parse_only;
-    notation_modifiers():m_persistent(true), m_parse_only(false) {}
+    notation_modifiers():m_parse_only(false) {}
     void parse(parser & p) {
         while (true) {
-            if (p.curr_is_token(get_local_tk())) {
-                p.next();
-                m_persistent = false;
-            } else if (p.curr_is_token(get_parsing_only_tk())) {
+            if (p.curr_is_token(get_parsing_only_tk())) {
                 p.next();
                 m_parse_only = true;
             } else {
@@ -628,93 +624,108 @@ struct notation_modifiers {
     }
 };
 
-static environment notation_cmd_core(parser & p, bool overload, bool reserve) {
-    check_not_in_parametric_section(p);
+static environment notation_cmd_core(parser & p, bool overload, bool reserve, bool persistent) {
+    if (persistent)
+        check_not_in_parametric_section(p);
     notation_modifiers mods;
     mods.parse(p);
-    flet<bool> set_allow_local(g_allow_local, in_context(p.env()) || !mods.m_persistent);
+    flet<bool> set_allow_local(g_allow_local, in_context(p.env()) || !persistent);
     environment env = p.env();
     buffer<token_entry> new_tokens;
     auto ne = parse_notation_core(p, overload, reserve, new_tokens, mods.m_parse_only);
     for (auto const & te : new_tokens)
-        env = add_user_token(env, te, mods.m_persistent);
-    env = add_notation(env, ne, mods.m_persistent);
+        env = add_user_token(env, te, persistent);
+    env = add_notation(env, ne, persistent);
     return env;
 }
 
-static environment mixfix_cmd(parser & p, mixfix_kind k, bool overload, bool reserve) {
-    check_not_in_parametric_section(p);
+static environment mixfix_cmd(parser & p, mixfix_kind k, bool overload, bool reserve, bool persistent) {
+    if (persistent)
+        check_not_in_parametric_section(p);
     notation_modifiers mods;
     mods.parse(p);
-    flet<bool> set_allow_local(g_allow_local, in_context(p.env()) || !mods.m_persistent);
+    flet<bool> set_allow_local(g_allow_local, in_context(p.env()) || !persistent);
     auto nt = parse_mixfix_notation(p, k, overload, reserve, mods.m_parse_only);
     environment env = p.env();
     if (nt.second)
-        env = add_user_token(env, *nt.second, mods.m_persistent);
-    env = add_notation(env, nt.first, mods.m_persistent);
+        env = add_user_token(env, *nt.second, persistent);
+    env = add_notation(env, nt.first, persistent);
     return env;
 }
 
 static environment notation_cmd(parser & p) {
     bool overload = !in_context(p.env());
     bool reserve  = false;
-    return notation_cmd_core(p, overload, reserve);
+    bool persistent = true;
+    return notation_cmd_core(p, overload, reserve, persistent);
 }
 
 static environment infixl_cmd(parser & p) {
     bool overload = !in_context(p.env());
     bool reserve  = false;
-    return mixfix_cmd(p, mixfix_kind::infixl, overload, reserve);
+    bool persistent = true;
+    return mixfix_cmd(p, mixfix_kind::infixl, overload, reserve, persistent);
 }
 
 static environment infixr_cmd(parser & p) {
     bool overload = !in_context(p.env());
     bool reserve  = false;
-    return mixfix_cmd(p, mixfix_kind::infixr, overload, reserve);
+    bool persistent = true;
+    return mixfix_cmd(p, mixfix_kind::infixr, overload, reserve, persistent);
 }
 
 static environment postfix_cmd(parser & p) {
     bool overload = !in_context(p.env());
     bool reserve  = false;
-    return mixfix_cmd(p, mixfix_kind::postfix, overload, reserve);
+    bool persistent = true;
+    return mixfix_cmd(p, mixfix_kind::postfix, overload, reserve, persistent);
 }
 
 static environment prefix_cmd(parser & p) {
     bool overload = !in_context(p.env());
     bool reserve  = false;
-    return mixfix_cmd(p, mixfix_kind::prefix, overload, reserve);
+    bool persistent = true;
+    return mixfix_cmd(p, mixfix_kind::prefix, overload, reserve, persistent);
+}
+
+// auxiliary procedure used by local_notation_cmd and reserve_cmd
+static environment dispatch_notation_cmd(parser & p, bool overload, bool reserve, bool persistent) {
+    if (p.curr_is_token(get_notation_tk())) {
+        p.next();
+        return notation_cmd_core(p, overload, reserve, persistent);
+    } else if (p.curr_is_token(get_infixl_tk())) {
+        p.next();
+        return mixfix_cmd(p, mixfix_kind::infixl, overload, reserve, persistent);
+    } else if (p.curr_is_token(get_infix_tk())) {
+        p.next();
+        return mixfix_cmd(p, mixfix_kind::infixl, overload, reserve, persistent);
+    } else if (p.curr_is_token(get_infixr_tk())) {
+        p.next();
+        return mixfix_cmd(p, mixfix_kind::infixr, overload, reserve, persistent);
+    } else if (p.curr_is_token(get_prefix_tk())) {
+        p.next();
+        return mixfix_cmd(p, mixfix_kind::prefix, overload, reserve, persistent);
+    } else if (p.curr_is_token(get_postfix_tk())) {
+        p.next();
+        return mixfix_cmd(p, mixfix_kind::postfix, overload, reserve, persistent);
+    } else {
+        throw parser_error("invalid local/reserve notation, 'infix', 'infixl', 'infixr', 'prefix', "
+                           "'postfix' or 'notation' expected", p.pos());
+    }
 }
 
 environment local_notation_cmd(parser & p) {
-    // TODO(Leo)
-    return p.env();
+    bool overload   = !in_context(p.env());
+    bool reserve    = false;
+    bool persistent = false;
+    return dispatch_notation_cmd(p, overload, reserve, persistent);
 }
 
 static environment reserve_cmd(parser & p) {
-    bool overload = false;
-    bool reserve  = true;
-    if (p.curr_is_token(get_notation_tk())) {
-        p.next();
-        return notation_cmd_core(p, overload, reserve);
-    } else if (p.curr_is_token(get_infixl_tk())) {
-        p.next();
-        return mixfix_cmd(p, mixfix_kind::infixl, overload, reserve);
-    } else if (p.curr_is_token(get_infix_tk())) {
-        p.next();
-        return mixfix_cmd(p, mixfix_kind::infixl, overload, reserve);
-    } else if (p.curr_is_token(get_infixr_tk())) {
-        p.next();
-        return mixfix_cmd(p, mixfix_kind::infixr, overload, reserve);
-    } else if (p.curr_is_token(get_prefix_tk())) {
-        p.next();
-        return mixfix_cmd(p, mixfix_kind::prefix, overload, reserve);
-    } else if (p.curr_is_token(get_postfix_tk())) {
-        p.next();
-        return mixfix_cmd(p, mixfix_kind::postfix, overload, reserve);
-    } else {
-        throw parser_error("invalid reserve notation, 'infix', 'infixl', 'infixr', 'prefix', "
-                           "'postfix' or 'notation' expected", p.pos());
-    }
+    bool overload   = false;
+    bool reserve    = true;
+    bool persistent = true;
+    return dispatch_notation_cmd(p, overload, reserve, persistent);
 }
 
 static environment precedence_cmd(parser & p) {
diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp
index 04ce298f6c..6cb3b738b2 100644
--- a/src/frontends/lean/token_table.cpp
+++ b/src/frontends/lean/token_table.cpp
@@ -90,7 +90,7 @@ void init_token_table(token_table & t) {
         {"theorem", "axiom", "variable", "protected", "private", "opaque", "definition", "example", "coercion",
          "variables", "parameter", "parameters", "constant", "constants", "[persistent]", "[visible]", "[instance]",
          "[off]", "[on]", "[none]", "[class]", "[coercion]", "[reducible]", "[irreducible]", "[parsing-only]", "[multiple-instances]",
-         "evaluate", "check", "eval", "[wf]", "[whnf]", "[strict]", "[local]", "[priority", "print", "end", "namespace", "section", "prelude",
+         "evaluate", "check", "eval", "[wf]", "[whnf]", "[strict]", "[priority", "print", "end", "namespace", "section", "prelude",
          "import", "inductive", "record", "structure", "module", "universe", "universes", "local",
          "precedence", "reserve", "infixl", "infixr", "infix", "postfix", "prefix", "notation", "context",
          "exit", "set_option", "open", "export", "calc_subst", "calc_refl", "calc_trans", "calc_symm", "tactic_hint",
diff --git a/src/frontends/lean/tokens.cpp b/src/frontends/lean/tokens.cpp
index a6fca3bf76..5bc7a35ba5 100644
--- a/src/frontends/lean/tokens.cpp
+++ b/src/frontends/lean/tokens.cpp
@@ -101,7 +101,6 @@ static name * g_prefix       = nullptr;
 static name * g_notation     = nullptr;
 static name * g_call         = nullptr;
 static name * g_persistent   = nullptr;
-static name * g_local        = nullptr;
 static name * g_root         = nullptr;
 static name * g_fields       = nullptr;
 static name * g_trust        = nullptr;
@@ -201,7 +200,6 @@ void initialize_tokens() {
     g_notation     = new name("notation");
     g_call         = new name("call");
     g_persistent   = new name("[persistent]");
-    g_local        = new name("[local]");
     g_root         = new name("_root_");
     g_fields       = new name("fields");
     g_trust        = new name("trust");
@@ -209,7 +207,6 @@ void initialize_tokens() {
 
 void finalize_tokens() {
     delete g_persistent;
-    delete g_local;
     delete g_root;
     delete g_fields;
     delete g_trust;
@@ -402,7 +399,6 @@ name const & get_prefix_tk() { return *g_prefix; }
 name const & get_notation_tk() { return *g_notation; }
 name const & get_call_tk() { return *g_call; }
 name const & get_persistent_tk() { return *g_persistent; }
-name const & get_local_tk() { return *g_local; }
 name const & get_root_tk() { return *g_root; }
 name const & get_fields_tk() { return *g_fields; }
 name const & get_trust_tk() { return *g_trust; }
diff --git a/src/frontends/lean/tokens.h b/src/frontends/lean/tokens.h
index a43277c9cc..2134e3e2ae 100644
--- a/src/frontends/lean/tokens.h
+++ b/src/frontends/lean/tokens.h
@@ -103,7 +103,6 @@ name const & get_prefix_tk();
 name const & get_notation_tk();
 name const & get_call_tk();
 name const & get_persistent_tk();
-name const & get_local_tk();
 name const & get_root_tk();
 name const & get_fields_tk();
 name const & get_trust_tk();
diff --git a/tests/lean/run/forest_height.lean b/tests/lean/run/forest_height.lean
index 53b7db492d..e045bb4ffe 100644
--- a/tests/lean/run/forest_height.lean
+++ b/tests/lean/run/forest_height.lean
@@ -33,7 +33,7 @@ inv_image lt tree_forest_height
 definition tree_forest.subterm.wf [instance] (A : Type) : well_founded (@tree_forest.subterm A) :=
 inv_image.wf tree_forest_height lt.wf
 
-infix [local] `≺`:50 := tree_forest.subterm
+local infix `≺`:50 := tree_forest.subterm
 
 definition tree_forest.height_lt.node {A : Type} (a : A) (f : forest A) : sum.inr f ≺ sum.inl (tree.node a f) :=
 have aux : forest.height f < tree.height (tree.node a f), from
diff --git a/tests/lean/run/local_notation.lean b/tests/lean/run/local_notation.lean
index 522b1233e1..2ab4497fb7 100644
--- a/tests/lean/run/local_notation.lean
+++ b/tests/lean/run/local_notation.lean
@@ -3,7 +3,7 @@ import logic
 section
   variables {A : Type}
   variables f : A → A → A
-  infixl [local] `+++`:10 := f
+  local infixl `+++`:10 := f
 
   variables a b c : A
   check f a b