diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp
index b9ccf7fa8..da67182d9 100644
--- a/src/frontends/lean/builtin_cmds.cpp
+++ b/src/frontends/lean/builtin_cmds.cpp
@@ -1154,7 +1154,7 @@ static environment app_builder_cmd(parser & p) {
     name c = p.check_constant_next("invalid #app_builder command, constant expected");
     bool has_mask = false;
     buffer<bool> mask;
-    if (p.curr_is_token(get_lparen_tk())) {
+    if (p.curr_is_token(get_lbracket_tk())) {
         p.next();
         has_mask = true;
         while (true) {
@@ -1164,7 +1164,7 @@ static environment app_builder_cmd(parser & p) {
                 break;
             p.next();
         }
-        p.check_token_next(get_rparen_tk(), "invalid #app_builder command, ')' expected");
+        p.check_token_next(get_rbracket_tk(), "invalid #app_builder command, ']' expected");
     }
 
     buffer<expr> args;
diff --git a/tests/lean/run/app_builder3.lean b/tests/lean/run/app_builder3.lean
index b43e9bc39..7580975bc 100644
--- a/tests/lean/run/app_builder3.lean
+++ b/tests/lean/run/app_builder3.lean
@@ -3,5 +3,5 @@ constant f : ∀ (A : Type) (a b c : A), a = c → A
 variables a b c : nat
 variables H : a = b
 
-#app_builder f (false, false, true, false, true) c, H
-#app_builder f (false, true, true, false, true) a, c, H
+#app_builder f [false, false, true, false, true] c, H
+#app_builder f [false, true, true, false, true] a, c, H