From 84df182bebffe0e5e318dc06bb404ac75c5333ff Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 20 Dec 2013 14:37:05 -0800
Subject: [PATCH] refactor(kernel/instantiate): remove hackish (dead) function

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

diff --git a/src/kernel/instantiate.cpp b/src/kernel/instantiate.cpp
index 784233352..97add18b0 100644
--- a/src/kernel/instantiate.cpp
+++ b/src/kernel/instantiate.cpp
@@ -12,7 +12,8 @@ Author: Leonardo de Moura
 #include "kernel/instantiate.h"
 
 namespace lean {
-expr instantiate_with_closed_relaxed(expr const & a, unsigned n, expr const * s, optional<metavar_env> const & menv) {
+expr instantiate_with_closed(expr const & a, unsigned n, expr const * s, optional<metavar_env> const & menv) {
+    lean_assert(std::all_of(s, s+n, [&](expr const & e) { return !has_free_var(e, 0, std::numeric_limits<unsigned>::max(), menv); }));
     return replace(a, [=](expr const & m, unsigned offset) -> expr {
             if (is_var(m)) {
                 unsigned vidx = var_idx(m);
@@ -34,16 +35,6 @@ expr instantiate_with_closed_relaxed(expr const & a, unsigned n, expr const * s,
             }
         });
 }
-expr instantiate_with_closed_relaxed(expr const & a, unsigned n, expr const * s, metavar_env const & menv) {
-    return instantiate_with_closed_relaxed(a, n, s, some_menv(menv));
-}
-expr instantiate_with_closed_relaxed(expr const & a, unsigned n, expr const * s) {
-    return instantiate_with_closed_relaxed(a, n, s, none_menv());
-}
-expr instantiate_with_closed(expr const & a, unsigned n, expr const * s, optional<metavar_env> const & menv) {
-    lean_assert(std::all_of(s, s+n, [&](expr const & e) { return !has_free_var(e, 0, std::numeric_limits<unsigned>::max(), menv); }));
-    return instantiate_with_closed_relaxed(a, n, s, menv);
-}
 expr instantiate_with_closed(expr const & e, unsigned n, expr const * s, metavar_env const & menv) { return instantiate_with_closed(e, n, s, some_menv(menv)); }
 expr instantiate_with_closed(expr const & e, unsigned n, expr const * s) { return instantiate_with_closed(e, n, s, none_menv()); }
 expr instantiate_with_closed(expr const & e, std::initializer_list<expr> const & l) { return instantiate_with_closed(e, l.size(), l.begin()); }
diff --git a/src/kernel/instantiate.h b/src/kernel/instantiate.h
index 7ca52288e..a5328eee2 100644
--- a/src/kernel/instantiate.h
+++ b/src/kernel/instantiate.h
@@ -25,15 +25,6 @@ expr instantiate_with_closed(expr const & e, expr const & s, optional<metavar_en
 expr instantiate_with_closed(expr const & e, expr const & s, metavar_env const & menv);
 expr instantiate_with_closed(expr const & e, expr const & s);
 
-/**
-   \brief Similar to instantiate_with_closed, but does not use an assertion for
-   testing whether arguments are close or not.
-   This version is useful, for example, when we want to treat metavariables as closed terms.
-*/
-expr instantiate_with_closed_relaxed(expr const & a, unsigned n, expr const * s, optional<metavar_env> const & menv);
-expr instantiate_with_closed_relaxed(expr const & a, unsigned n, expr const * s, metavar_env const & menv);
-expr instantiate_with_closed_relaxed(expr const & a, unsigned n, expr const * s);
-
 /**
    \brief Replace the free variables with indices 0, ..., n-1 with s[n-1], ..., s[0] in e.