chore: fix typo

2026-03-17 18:34:06 +00:00 · 2024-08-06 08:10:17 -07:00
1 changed files with 1 additions and 1 deletions
--- a/src/kernel/instantiate_mvars.cpp
+++ b/src/kernel/instantiate_mvars.cpp
@@ -206,7 +206,7 @@ class instantiate_mvars_fn {
    */
    expr visit_mvar_app_args(expr const & e) {
        if (is_app(e)) {
-            return update_app(e, visit_app_default(app_fn(e)), visit(app_arg(e)));
+            return update_app(e, visit_mvar_app_args(app_fn(e)), visit(app_arg(e)));
        } else {
            lean_assert(is_mvar(e));
            return e;