diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index e1d0384ea..e378b4cfc 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -556,10 +556,14 @@ expr elaborator::visit_sort(expr const & e) {
 }
 
 expr elaborator::visit_macro(expr const & e, constraint_seq & cs) {
-    buffer<expr> args;
-    for (unsigned i = 0; i < macro_num_args(e); i++)
-        args.push_back(visit(macro_arg(e, i), cs));
-    return update_macro(e, args.size(), args.data());
+    if (is_as_is(e)) {
+        return get_as_is_arg(e);
+    } else {
+        buffer<expr> args;
+        for (unsigned i = 0; i < macro_num_args(e); i++)
+            args.push_back(visit(macro_arg(e, i), cs));
+        return update_macro(e, args.size(), args.data());
+    }
 }
 
 expr elaborator::visit_constant(expr const & e) {
@@ -760,9 +764,7 @@ pair<expr, constraint_seq> elaborator::visit(expr const & e) {
     expr r;
     expr b = e;
     constraint_seq cs;
-    if (is_as_is(e)) {
-        r = get_as_is_arg(e);
-    } else if (is_explicit(e)) {
+    if (is_explicit(e)) {
         b    = get_explicit_arg(e);
         if (is_sorry(b)) {
             r = visit_constant(b);