From 565dbe170051e6420277bb781112746dffde44f8 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 17 Feb 2014 16:53:03 -0800
Subject: [PATCH] fix(kernel/instantiate): bug in new head_beta_reduce

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/kernel/instantiate.cpp | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/kernel/instantiate.cpp b/src/kernel/instantiate.cpp
index 010cdabf3..6918e60bf 100644
--- a/src/kernel/instantiate.cpp
+++ b/src/kernel/instantiate.cpp
@@ -96,6 +96,7 @@ expr head_beta_reduce(expr const & t) {
             expr const & f = app_fn(*it);
             args.push_back(app_arg(*it));
             if (is_lambda(f)) {
+                std::reverse(args.begin(), args.end());
                 return apply_beta(f, args.size(), args.data());
             } else {
                 lean_assert(is_app(f));