diff --git a/library/init/core.lean b/library/init/core.lean
index 5c9dbdee37..358822694e 100644
--- a/library/init/core.lean
+++ b/library/init/core.lean
@@ -336,7 +336,6 @@ inductive List (T : Type u)
 | cons (hd : T) (tl : List) : List
 
 infixr :: := List.cons
-notation `[` l:(foldr `, ` (h t, List.cons h t) List.nil `]`) := l
 
 inductive Nat
 | zero : Nat
diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp
index a11d9bef4b..3c47a75888 100644
--- a/src/frontends/lean/builtin_exprs.cpp
+++ b/src/frontends/lean/builtin_exprs.cpp
@@ -718,6 +718,28 @@ static expr parse_assume(parser & p, unsigned, expr const *, pos_info const & po
     }
 }
 
+static expr parse_list(parser & p, unsigned, expr const *, pos_info const & pos) {
+    buffer<expr> elems;
+    if (!p.curr_is_token(get_rbracket_tk())) {
+        while (true) {
+            expr elem = p.parse_expr();
+            elems.push_back(elem);
+            if (!p.curr_is_token(get_comma_tk()))
+                break;
+            p.next();
+        }
+    }
+    p.check_token_next(get_rbracket_tk(), "invalid list, ']' expected");
+    expr r = p.save_pos(mk_constant(get_list_nil_name()), pos);
+    unsigned i = elems.size();
+    while (i > 0) {
+        --i;
+        expr elem = elems[i];
+        r = p.save_pos(mk_app(mk_constant(get_list_cons_name()), elem, r), p.pos_of(elem));
+    }
+    return r;
+}
+
 static void consume_rparen(parser & p) {
     p.check_token_next(get_rparen_tk(), "invalid expression, `)` expected");
 }
@@ -955,6 +977,7 @@ parse_table init_nud_table() {
     r = r.add({transition("suffices", mk_ext_action(parse_suffices))}, x0);
     r = r.add({transition("if", mk_ext_action(parse_if_then_else))}, x0);
     r = r.add({transition("(", mk_ext_action(parse_lparen))}, x0);
+    r = r.add({transition("[", mk_ext_action(parse_list))}, x0);
     r = r.add({transition("⟨", mk_ext_action(parse_constructor))}, x0);
     r = r.add({transition("{", mk_ext_action(parse_curly_bracket))}, x0);
     r = r.add({transition(".(", mk_ext_action(parse_inaccessible))}, x0);
diff --git a/src/frontends/lean/notation_cmd.cpp b/src/frontends/lean/notation_cmd.cpp
index c994386d8c..70756175d3 100644
--- a/src/frontends/lean/notation_cmd.cpp
+++ b/src/frontends/lean/notation_cmd.cpp
@@ -328,34 +328,7 @@ static action parse_action(parser & p, name const & prev_token, unsigned default
             return mk_expr_action(get_precedence(p.env(), new_tokens, prev_token));
         } else {
             p.check_token_next(get_lparen_tk(), "invalid notation declaration, '(', numeral expected");
-            if (p.curr_is_token_or_id(get_foldl_tk()) || p.curr_is_token_or_id(get_foldr_tk())) {
-                bool is_fold_right = p.curr_is_token_or_id(get_foldr_tk());
-                p.next();
-                auto prec = parse_optional_precedence(p);
-                name sep  = parse_quoted_symbol_or_token(p, new_tokens);
-                expr rec;
-                {
-                    parser::local_scope scope(p);
-                    p.check_token_next(get_lparen_tk(), "invalid fold notation argument, '(' expected");
-                    parse_notation_local(p, locals);
-                    parse_notation_local(p, locals);
-                    p.check_token_next(get_comma_tk(),  "invalid fold notation argument, ',' expected");
-                    rec  = parse_notation_expr(p, locals);
-                    p.check_token_next(get_rparen_tk(), "invalid fold notation argument, ')' expected");
-                    locals.pop_back();
-                    locals.pop_back();
-                }
-                optional<expr> ini;
-                if (!p.curr_is_token(get_rparen_tk()) && !p.curr_is_quoted_symbol())
-                    ini = parse_notation_expr(p, locals);
-                optional<name> terminator;
-                if (!p.curr_is_token(get_rparen_tk()))
-                    terminator = parse_quoted_symbol_or_token(p, new_tokens);
-                p.check_token_next(get_rparen_tk(), "invalid fold notation argument, ')' expected");
-                return mk_exprs_action(sep, rec, ini, terminator, is_fold_right, prec ? *prec : 0);
-            } else {
-                throw parser_error("invalid notation declaration, 'foldl', 'foldr' expected", p.pos());
-            }
+            throw parser_error("invalid notation declaration", p.pos());
         }
     } else {
         return mk_expr_action(default_prec);