From 21daa18950e51bb36458c77778e380724cd855ea Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 28 Apr 2016 17:40:34 -0700 Subject: [PATCH] chore(compiler/simp_pr1_rec): cleanup --- src/compiler/simp_pr1_rec.cpp | 9 +-------- 1 file changed, 1 insertion(+), 8 deletions(-) diff --git a/src/compiler/simp_pr1_rec.cpp b/src/compiler/simp_pr1_rec.cpp index f72e0e4e81..f13d9bdc2d 100644 --- a/src/compiler/simp_pr1_rec.cpp +++ b/src/compiler/simp_pr1_rec.cpp @@ -15,7 +15,7 @@ Author: Leonardo de Moura #include "compiler/util.h" namespace lean { -class simp_pr1_rec_fn : public replace_visitor { +class simp_pr1_rec_fn : public replace_visitor_closed { environment m_env; type_checker m_tc; @@ -157,13 +157,6 @@ class simp_pr1_rec_fn : public replace_visitor { return replace_visitor::visit_app(e); } - virtual expr visit_binding(expr const & b) { - expr new_domain = visit(binding_domain(b)); - expr l = mk_local(mk_fresh_name(), new_domain); - expr new_body = abstract_local(visit(instantiate(binding_body(b), l)), l); - return update_binding(b, new_domain, new_body); - } - public: simp_pr1_rec_fn(environment const & env):m_env(env), m_tc(env) {} };