From 5687c249440cb09498cc4c015b06fd6edc047677 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 22 Jun 2015 10:23:54 -0700
Subject: [PATCH] refactor(library/tactic/induction_tactic): cleanup

---
 src/library/reducible.h                 |  1 -
 src/library/tactic/induction_tactic.cpp | 37 ++++++-------------------
 2 files changed, 8 insertions(+), 30 deletions(-)

diff --git a/src/library/reducible.h b/src/library/reducible.h
index b89a0894d..5d59806ab 100644
--- a/src/library/reducible.h
+++ b/src/library/reducible.h
@@ -7,7 +7,6 @@ Author: Leonardo de Moura
 #pragma once
 #include <memory>
 #include "kernel/type_checker.h"
-#include "kernel/default_converter.h"
 #include "library/util.h"
 
 namespace lean {
diff --git a/src/library/tactic/induction_tactic.cpp b/src/library/tactic/induction_tactic.cpp
index 68219401d..d444fe0f2 100644
--- a/src/library/tactic/induction_tactic.cpp
+++ b/src/library/tactic/induction_tactic.cpp
@@ -7,6 +7,7 @@ Author: Leonardo de Moura
 #include "kernel/abstract.h"
 #include "kernel/instantiate.h"
 #include "kernel/inductive/inductive.h"
+#include "kernel/default_converter.h"
 #include "library/util.h"
 #include "library/user_recursors.h"
 #include "library/constants.h"
@@ -18,28 +19,6 @@ Author: Leonardo de Moura
 #include "library/tactic/generalize_tactic.h"
 
 namespace lean {
-class rec_opaque_converter : public default_converter {
-    name m_I;
-public:
-    rec_opaque_converter(environment const & env, name const & I):default_converter(env), m_I(I) {}
-    virtual bool is_opaque(declaration const & d) const {
-        if (d.get_name() == m_I)
-            return true;
-        return default_converter::is_opaque(d);
-    }
-};
-
-class has_rec_opaque_converter : public default_converter {
-    has_recursors_pred m_pred;
-public:
-    has_rec_opaque_converter(environment const & env):default_converter(env), m_pred(env) {}
-    virtual bool is_opaque(declaration const & d) const {
-        if (m_pred(d.get_name()))
-            return true;
-        return default_converter::is_opaque(d);
-    }
-};
-
 class induction_tac {
     environment const &   m_env;
     io_state const &      m_ios;
@@ -307,14 +286,14 @@ public:
     expr normalize_H_type(expr const & H) {
         lean_assert(is_local(H));
         if (m_rec_name) {
-            recursor_info info = get_recursor_info(m_env, *m_rec_name);
-            type_checker aux_tc(m_env, m_ngen.mk_child(),
-                                std::unique_ptr<converter>(new rec_opaque_converter(m_env, info.get_type_name())));
-            return aux_tc.whnf(mlocal_type(H)).first;
+            recursor_info info      = get_recursor_info(m_env, *m_rec_name);
+            name tname              = info.get_type_name();
+            type_checker_ptr aux_tc = mk_type_checker(m_env, m_ngen.mk_child(), [=](name const & n) { return n == tname; });
+            return aux_tc->whnf(mlocal_type(H)).first;
         } else {
-            type_checker aux_tc(m_env, m_ngen.mk_child(),
-                                std::unique_ptr<converter>(new has_rec_opaque_converter(m_env)));
-            return aux_tc.whnf(mlocal_type(H)).first;
+            has_recursors_pred pred(m_env);
+            type_checker_ptr aux_tc = mk_type_checker(m_env, m_ngen.mk_child(), pred);
+            return aux_tc->whnf(mlocal_type(H)).first;
         }
     }