From 1398c927cde05e81c351bb182e932ca8f0b3f9e9 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 24 Jul 2013 00:50:58 -0700
Subject: [PATCH] Fix compilation error with clang++

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/kernel/abstract.cpp    | 4 ++--
 src/kernel/instantiate.cpp | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/kernel/abstract.cpp b/src/kernel/abstract.cpp
index 63ba556aa..25aee248f 100644
--- a/src/kernel/abstract.cpp
+++ b/src/kernel/abstract.cpp
@@ -12,7 +12,7 @@ namespace lean {
 expr abstract(unsigned n, expr const * s, expr const & e) {
     lean_assert(std::all_of(s, s+n, closed));
 
-    auto f = [=](expr const & e, unsigned offset) {
+    auto f = [=](expr const & e, unsigned offset) -> expr {
         unsigned i = n;
         while (i > 0) {
             --i;
@@ -27,7 +27,7 @@ expr abstract(unsigned n, expr const * s, expr const & e) {
 expr abstract_p(unsigned n, expr const * s, expr const & e) {
     lean_assert(std::all_of(s, s+n, closed));
 
-    auto f = [=](expr const & e, unsigned offset) {
+    auto f = [=](expr const & e, unsigned offset) -> expr {
         unsigned i = n;
         while (i > 0) {
             --i;
diff --git a/src/kernel/instantiate.cpp b/src/kernel/instantiate.cpp
index c99df07f6..dd54af0a3 100644
--- a/src/kernel/instantiate.cpp
+++ b/src/kernel/instantiate.cpp
@@ -12,7 +12,7 @@ namespace lean {
 expr instantiate(unsigned n, expr const * s, expr const & e) {
     lean_assert(std::all_of(s, s+n, closed));
 
-    auto f = [=](expr const & e, unsigned offset) {
+    auto f = [=](expr const & e, unsigned offset) -> expr {
         if (is_var(e)) {
             unsigned vidx = var_idx(e);
             if (vidx >= offset) {