diff --git a/src/library/equations_compiler/compiler.cpp b/src/library/equations_compiler/compiler.cpp
index 4b0bf79eaf..86db3840d4 100644
--- a/src/library/equations_compiler/compiler.cpp
+++ b/src/library/equations_compiler/compiler.cpp
@@ -29,6 +29,8 @@ expr compile_equations(environment & env, options const & opts, metavar_context
     optional<expr> eqns1 = try_structural_rec(ctx.get(), eqns, arg_idx);
     if (eqns1) {
         elim_match(env, opts, mctx, lctx, *eqns1);
+    } else if (!is_recursive_eqns(ctx, eqns)) {
+        elim_match(env, opts, mctx, lctx, eqns);
     }
 
     // test unbounded_rec