diff --git a/src/kernel/normalize.cpp b/src/kernel/normalize.cpp
index 5fed106482..8967cd929a 100644
--- a/src/kernel/normalize.cpp
+++ b/src/kernel/normalize.cpp
@@ -174,18 +174,9 @@ public:
         unsigned k = length(m_ctx);
         return reify(normalize(e, stack(), k), k);
     }
-
-    expr operator()(expr const & e, expr const & v) {
-        unsigned k = length(m_ctx);
-        stack s = extend(stack(), normalize(v, stack(), k));
-        return reify(normalize(e, s, k+1), k+1);
-    }
 };
 
 expr normalize(expr const & e, environment const & env, context const & ctx) {
     return normalize_fn(env, ctx)(e);
 }
-expr normalize(expr const & e, environment const & env, context const & ctx, expr const & v) {
-    return normalize_fn(env, ctx)(e, v);
-}
 }
diff --git a/src/kernel/normalize.h b/src/kernel/normalize.h
index 597b60f3b0..707b08e1b9 100644
--- a/src/kernel/normalize.h
+++ b/src/kernel/normalize.h
@@ -13,6 +13,4 @@ namespace lean {
 class environment;
 /** \brief Normalize e using the environment env and context ctx */
 expr normalize(expr const & e, environment const & env, context const & ctx = context());
-/** \brief Normalize e using the environment env, context ctx, and add v to "normalization stack" */
-expr normalize(expr const & e, environment const & env, context const & ctx, expr const & v);
 }
diff --git a/src/kernel/type_check.cpp b/src/kernel/type_check.cpp
index bd4b5fac46..a8487bf742 100644
--- a/src/kernel/type_check.cpp
+++ b/src/kernel/type_check.cpp
@@ -20,10 +20,6 @@ class infer_type_fn {
         return ::lean::normalize(e, m_env, ctx);
     }
 
-    expr normalize(expr const & e, context const & ctx, expr const & v) {
-        return ::lean::normalize(e, m_env, ctx, v);
-    }
-
     expr lookup(context const & c, unsigned i) {
         context const & def_c = ::lean::lookup(c, i);
         lean_assert(length(c) >= length(def_c));