diff --git a/src/kernel/default_converter.cpp b/src/kernel/default_converter.cpp
index e45695366..e4353ce87 100644
--- a/src/kernel/default_converter.cpp
+++ b/src/kernel/default_converter.cpp
@@ -24,6 +24,9 @@ default_converter::default_converter(environment const & env, optional<module_id
 default_converter::default_converter(environment const & env, optional<module_idx> mod_idx, bool memoize):
     default_converter(env, mod_idx, memoize, [](name const &) { return false; }) {}
 
+default_converter::default_converter(environment const & env, bool relax_main_opaque, bool memoize):
+    default_converter(env, relax_main_opaque ? optional<module_idx>(0) : optional<module_idx>(), memoize) {}
+
 constraint default_converter::mk_eq_cnstr(expr const & lhs, expr const & rhs, justification const & j) {
     return ::lean::mk_eq_cnstr(lhs, rhs, j, static_cast<bool>(m_module_idx));
 }
diff --git a/src/kernel/default_converter.h b/src/kernel/default_converter.h
index 235381ccf..c6f35056d 100644
--- a/src/kernel/default_converter.h
+++ b/src/kernel/default_converter.h
@@ -74,7 +74,8 @@ protected:
 public:
     default_converter(environment const & env, optional<module_idx> mod_idx, bool memoize,
                       extra_opaque_pred const & pred);
-    default_converter(environment const & env, optional<module_idx> mod_idx, bool memoize);
+    default_converter(environment const & env, optional<module_idx> mod_idx, bool memoize = true);
+    default_converter(environment const & env, bool relax_main_opaque, bool memoize = true);
 
     virtual bool is_opaque(declaration const & d) const;
     virtual optional<module_idx> get_module_idx() const { return m_module_idx; }
diff --git a/src/library/tactic/rewrite_tactic.cpp b/src/library/tactic/rewrite_tactic.cpp
index 64455c9da..ee0c02462 100644
--- a/src/library/tactic/rewrite_tactic.cpp
+++ b/src/library/tactic/rewrite_tactic.cpp
@@ -13,6 +13,7 @@ Author: Leonardo de Moura
 #include "kernel/abstract.h"
 #include "kernel/replace_fn.h"
 #include "kernel/for_each_fn.h"
+#include "kernel/default_converter.h"
 #include "kernel/inductive/inductive.h"
 #include "library/normalize.h"
 #include "library/kernel_serializer.h"
@@ -479,22 +480,29 @@ class rewrite_fn {
         return m_g.mk_meta(m_ngen.next(), type);
     }
 
+    class rewriter_converter : public default_converter {
+        list<name> const & m_to_unfold;
+        bool             & m_unfolded;
+    public:
+        rewriter_converter(environment const & env, bool relax_main_opaque, list<name> const & to_unfold,
+                           bool & unfolded):
+            default_converter(env, relax_main_opaque),
+            m_to_unfold(to_unfold), m_unfolded(unfolded) {}
+        virtual bool is_opaque(declaration const & d) const {
+            if (std::find(m_to_unfold.begin(), m_to_unfold.end(), d.get_name()) != m_to_unfold.end()) {
+                m_unfolded = true;
+                return false;
+            } else {
+                return true;
+            }
+        }
+    };
+
     optional<expr> reduce(expr const & e, list<name> const & to_unfold) {
-        bool unfolded = !to_unfold;
-        extra_opaque_pred pred([&](name const & n) {
-                // everything is opaque but to_unfold
-                if (std::find(to_unfold.begin(), to_unfold.end(), n) != to_unfold.end()) {
-                    unfolded = true;
-                    return false;
-                } else {
-                    return true;
-                }
-            });
+        bool unfolded          = !to_unfold;
         bool relax_main_opaque = false;
-        bool memoize           = true;
         auto tc = new type_checker(m_env, m_ngen.mk_child(),
-                                   mk_default_converter(m_env, relax_main_opaque,
-                                                        memoize, pred));
+                                   std::unique_ptr<converter>(new rewriter_converter(m_env, relax_main_opaque, to_unfold, unfolded)));
         constraint_seq cs;
         expr r = normalize(*tc, e, cs);
         if (!unfolded || cs) // FAIL if didn't unfolded or generated constraints