diff --git a/library/algebra/interval.lean b/library/algebra/interval.lean
index 98ba3bcad..c3c4373f7 100644
--- a/library/algebra/interval.lean
+++ b/library/algebra/interval.lean
@@ -32,14 +32,14 @@ definition Icu (a : A)   : set A := {x | a ≤ x}
 definition Iuo (b : A)   : set A := {x | x < b}
 definition Iuc (b : A)   : set A := {x | x ≤ b}
 
-notation `'` `(` a `, ` b `)`     := Ioo a b
-notation `'` `(` a `, ` b `]`     := Ioc a b
-notation `'[` a `, ` b `)`        := Ico a b
-notation `'[` a `, ` b `]`       := Icc a b
-notation `'` `(` a `, ` `∞` `)`   := Iou a
-notation `'[` a `, ` `∞` `)`      := Icu a
-notation `'` `(` `-∞` `, ` b `)`  := Iuo b
-notation `'` `(` `-∞` `, ` b `]`  := Iuc b
+notation `'(` a `, ` b `)`     := Ioo a b
+notation `'(` a `, ` b `]`     := Ioc a b
+notation `'[` a `, ` b `)`     := Ico a b
+notation `'[` a `, ` b `]`     := Icc a b
+notation `'(` a `, ` `∞` `)`   := Iou a
+notation `'[` a `, ` `∞` `)`   := Icu a
+notation `'(` `-∞` `, ` b `)`  := Iuo b
+notation `'(` `-∞` `, ` b `]`  := Iuc b
 
 variables a b : A
 
diff --git a/src/frontends/lean/notation_cmd.cpp b/src/frontends/lean/notation_cmd.cpp
index c6770b0f6..b193cc448 100644
--- a/src/frontends/lean/notation_cmd.cpp
+++ b/src/frontends/lean/notation_cmd.cpp
@@ -662,9 +662,16 @@ notation_entry parse_notation(parser & p, bool overload, buffer<token_entry> & n
     return parse_notation(p, overload, grp, new_tokens, allow_local);
 }
 
-static char g_reserved_chars[] = {'(', ')', ',', 0};
+static char g_reserved_chars[] = {',', 0};
 
 static void check_token(char const * tk) {
+    if (!tk || !*tk)
+        throw exception("invalid null token");
+    if (tk[0] == '(')
+        throw exception(sstream() << "invalid token `" << tk << "`, it starts with '('");
+    unsigned sz = strlen(tk);
+    if (tk[sz-1] == ')')
+        throw exception(sstream() << "invalid token `" << tk << "`, it ends with ')'");
     while (tk && *tk) {
         unsigned sz = get_utf8_size(*tk);
         if (sz == 0) {
diff --git a/tests/lean/notation5.lean.expected.out b/tests/lean/notation5.lean.expected.out
index 9234397c5..b695d7e75 100644
--- a/tests/lean/notation5.lean.expected.out
+++ b/tests/lean/notation5.lean.expected.out
@@ -1,5 +1,5 @@
-notation5.lean:3:0: error: invalid token `((`, it contains reserved character `(`
-notation5.lean:5:0: error: invalid token `(`, it contains reserved character `(`
-notation5.lean:7:0: error: invalid token `))`, it contains reserved character `)`
+notation5.lean:3:0: error: invalid token `((`, it starts with '('
+notation5.lean:5:0: error: invalid token `(`, it starts with '('
+notation5.lean:7:0: error: invalid token `))`, it ends with ')'
 notation5.lean:9:0: error: invalid token `,,`, it contains reserved character `,`
 notation5.lean:11:0: error: invalid token `,`, it contains reserved character `,`