diff --git a/src/library/equations_compiler/equations.cpp b/src/library/equations_compiler/equations.cpp
index 3f63940291..18fc16c800 100644
--- a/src/library/equations_compiler/equations.cpp
+++ b/src/library/equations_compiler/equations.cpp
@@ -192,6 +192,17 @@ expr update_equations(expr const & eqns, buffer<expr> const & new_eqs) {
     }
 }
 
+expr update_equations(expr const & eqns, equations_header const & header) {
+    buffer<expr> eqs;
+    to_equations(eqns, eqs);
+    if (is_wf_equations(eqns)) {
+        return copy_tag(eqns, mk_equations(header, eqs.size(), eqs.data(),
+                                           equations_wf_rel(eqns), equations_wf_proof(eqns)));
+    } else {
+        return copy_tag(eqns, mk_equations(header, eqs.size(), eqs.data()));
+    }
+}
+
 // LEGACY
 expr mk_equations(unsigned num_fns, unsigned num_eqs, expr const * eqs) {
     return mk_equations(equations_header(num_fns), num_eqs, eqs);
diff --git a/src/library/equations_compiler/equations.h b/src/library/equations_compiler/equations.h
index 71cfb1e9e5..ec8a9b0c21 100644
--- a/src/library/equations_compiler/equations.h
+++ b/src/library/equations_compiler/equations.h
@@ -48,6 +48,7 @@ struct equations_header {
 expr mk_equations(equations_header const & header, unsigned num_eqs, expr const * eqs, expr const & R, expr const & Hwf);
 expr mk_equations(equations_header const & header, unsigned num_eqs, expr const * eqs);
 expr update_equations(expr const & eqns, buffer<expr> const & new_eqs);
+expr update_equations(expr const & eqns, equations_header const & header);
 
 bool is_equations(expr const & e);
 bool is_wf_equations(expr const & e);
diff --git a/src/library/equations_compiler/wf_rec.cpp b/src/library/equations_compiler/wf_rec.cpp
index cbc07b395e..d867c2f89d 100644
--- a/src/library/equations_compiler/wf_rec.cpp
+++ b/src/library/equations_compiler/wf_rec.cpp
@@ -454,6 +454,10 @@ struct wf_rec_fn {
         equations_header const & header = get_equations_header(eqns);
         if (header.m_num_fns > 1) {
             eqns = pack_mutual(eqns);
+        } else {
+            equations_header new_header = header;
+            new_header.m_fn_names       = to_list(name(head(header.m_fn_names), "_pack"));
+            eqns                        = update_equations(eqns, new_header);
         }
 
         /* Retrieve well founded relation */
diff --git a/tests/lean/eqn_hole.lean.expected.out b/tests/lean/eqn_hole.lean.expected.out
index 647e48b03b..fdbc6c2e55 100644
--- a/tests/lean/eqn_hole.lean.expected.out
+++ b/tests/lean/eqn_hole.lean.expected.out
@@ -8,4 +8,3 @@ context:
 g : ℕ → ℕ,
 n : ℕ
 ⊢ ℕ
-eqn_hole.lean:6:11: error: support for well-founded recursion has not been implemented yet, use 'set_option trace.eqn_compiler true' for additional information