From ca059107cf96fb9f6cde6d128805eb0414b658ff Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 29 Sep 2015 10:42:00 -0700
Subject: [PATCH] fix(library/blast/state): incorrect 'replace'

---
 src/library/blast/state.cpp | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/library/blast/state.cpp b/src/library/blast/state.cpp
index 3319ca80c7..6be392baeb 100644
--- a/src/library/blast/state.cpp
+++ b/src/library/blast/state.cpp
@@ -6,6 +6,7 @@ Author: Leonardo de Moura
 */
 #include "kernel/abstract.h"
 #include "kernel/for_each_fn.h"
+#include "kernel/replace_fn.h"
 #include "library/blast/state.h"
 
 namespace lean {
@@ -43,7 +44,7 @@ goal state::to_goal(branch const & b) const {
     metavar_idx_map<expr>    midx2meta;
     name M("M");
     std::function<expr(expr const &)> convert = [&](expr const & e) {
-        return replace(e, [&](expr const & e) {
+        return lean::replace(e, [&](expr const & e) {
                 if (is_lref(e)) {
                     auto r = hidx2local.find(lref_index(e));
                     lean_assert(r);