From d0bc4e4245536fe6f9cc128c24981be775b9e1e8 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 20 Jul 2024 06:20:43 +0200 Subject: [PATCH] fix: `replace_fn.cpp` (#4798) --- src/kernel/replace_fn.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/kernel/replace_fn.cpp b/src/kernel/replace_fn.cpp index 23883f1d8b..65b9a07dc2 100644 --- a/src/kernel/replace_fn.cpp +++ b/src/kernel/replace_fn.cpp @@ -105,7 +105,7 @@ class replace_fn { lean_inc_ref(m_f); lean_object * r = lean_apply_1(m_f, e.raw()); if (!lean_is_scalar(r)) { - expr e_new(lean_ctor_get(r, 0)); + expr e_new(lean_ctor_get(r, 0), true); lean_dec_ref(r); return save_result(e, e_new, shared); }