diff --git a/library/init/meta/simp_tactic.lean b/library/init/meta/simp_tactic.lean
index a90539b8ab..0f332cb58a 100644
--- a/library/init/meta/simp_tactic.lean
+++ b/library/init/meta/simp_tactic.lean
@@ -49,7 +49,10 @@ meta def simp_lemmas.rewrite : simp_lemmas → tactic unit → name → expr →
 simp_lemmas.rewrite_core reducible
 
 /- (simp_lemmas.drewrite s e) tries to rewrite 'e' using only refl lemmas in 's' -/
-meta constant simp_lemmas.drewrite : simp_lemmas → expr → tactic expr
+meta constant simp_lemmas.drewrite_core : transparency → simp_lemmas → expr → tactic expr
+
+meta def simp_lemmas.drewrite : simp_lemmas → expr → tactic expr :=
+simp_lemmas.drewrite_core reducible
 
 /- Simplify the given expression using [simp] and [congr] lemmas.
    The first argument is a tactic to be used to discharge proof obligations.
diff --git a/src/frontends/lean/definition_cmds.cpp b/src/frontends/lean/definition_cmds.cpp
index 90b021444e..f1f7448288 100644
--- a/src/frontends/lean/definition_cmds.cpp
+++ b/src/frontends/lean/definition_cmds.cpp
@@ -23,10 +23,10 @@ Author: Leonardo de Moura
 #include "library/error_handling.h"
 #include "library/scope_pos_info_provider.h"
 #include "library/replace_visitor.h"
-#include "library/eqn_lemmas.h"
 #include "library/equations_compiler/equations.h"
 #include "library/compiler/vm_compiler.h"
 #include "library/compiler/rec_fn_macro.h"
+#include "library/tactic/eqn_lemmas.h"
 #include "frontends/lean/parser.h"
 #include "frontends/lean/tokens.h"
 #include "frontends/lean/elaborator.h"
diff --git a/src/frontends/lean/print_cmd.cpp b/src/frontends/lean/print_cmd.cpp
index 9ae82e4c1b..f7c9f62e84 100644
--- a/src/frontends/lean/print_cmd.cpp
+++ b/src/frontends/lean/print_cmd.cpp
@@ -24,7 +24,7 @@ Author: Leonardo de Moura
 #include "library/type_context.h"
 #include "library/unification_hint.h"
 #include "library/reducible.h"
-#include "library/simp_lemmas.h"
+#include "library/tactic/simp_lemmas.h"
 #include "library/tactic/kabstract.h"
 #include "frontends/lean/parser.h"
 #include "frontends/lean/util.h"
diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt
index e2ac35bbb6..3f2257e6f5 100644
--- a/src/library/CMakeLists.txt
+++ b/src/library/CMakeLists.txt
@@ -15,5 +15,4 @@ add_library(library OBJECT deep_copy.cpp expr_lt.cpp io_state.cpp
   fun_info.cpp congr_lemma.cpp defeq_canonizer.cpp scope_pos_info_provider.cpp
   mpq_macro.cpp arith_instance_manager.cpp replace_visitor_with_tc.cpp
   aux_definition.cpp inverse.cpp library_system.cpp pattern_attribute.cpp choice.cpp
-  locals.cpp normalize.cpp discr_tree.cpp simp_lemmas.cpp eqn_lemmas.cpp
-  )
+  locals.cpp normalize.cpp discr_tree.cpp)
diff --git a/src/library/constructions/has_sizeof.cpp b/src/library/constructions/has_sizeof.cpp
index ec570f6334..b5c8f13435 100644
--- a/src/library/constructions/has_sizeof.cpp
+++ b/src/library/constructions/has_sizeof.cpp
@@ -23,7 +23,7 @@ Author: Daniel Selsam
 #include "library/trace.h"
 #include "library/module.h"
 #include "library/constants.h"
-#include "library/simp_lemmas.h"
+#include "library/tactic/simp_lemmas.h"
 #include "library/constructions/has_sizeof.h"
 
 namespace lean {
diff --git a/src/library/constructions/has_sizeof.h b/src/library/constructions/has_sizeof.h
index dd50df952f..c161425e2c 100644
--- a/src/library/constructions/has_sizeof.h
+++ b/src/library/constructions/has_sizeof.h
@@ -6,7 +6,7 @@ Author: Daniel Selsam
 */
 #pragma once
 #include "kernel/environment.h"
-#include "library/simp_lemmas.h"
+#include "library/tactic/simp_lemmas.h"
 
 namespace lean {
 /** \brief Given an inductive datatype \c n in \c env, add
diff --git a/src/library/equations_compiler/util.cpp b/src/library/equations_compiler/util.cpp
index 2aa677c5fe..9a9ab9cba3 100644
--- a/src/library/equations_compiler/util.cpp
+++ b/src/library/equations_compiler/util.cpp
@@ -18,9 +18,9 @@ Author: Leonardo de Moura
 #include "library/inverse.h"
 #include "library/replace_visitor.h"
 #include "library/aux_definition.h"
-#include "library/eqn_lemmas.h"
 #include "library/scope_pos_info_provider.h"
 #include "library/compiler/vm_compiler.h"
+#include "library/tactic/eqn_lemmas.h"
 #include "library/equations_compiler/equations.h"
 #include "library/equations_compiler/util.h"
 
diff --git a/src/library/inductive_compiler/nested.cpp b/src/library/inductive_compiler/nested.cpp
index 339d6bb15f..d50d491c5f 100644
--- a/src/library/inductive_compiler/nested.cpp
+++ b/src/library/inductive_compiler/nested.cpp
@@ -29,7 +29,7 @@ Author: Daniel Selsam
 #include "library/protected.h"
 #include "library/attribute_manager.h"
 #include "library/pattern_attribute.h"
-#include "library/simp_lemmas.h"
+#include "library/tactic/simp_lemmas.h"
 #include "library/constructions/has_sizeof.h"
 #include "library/inductive_compiler/ginductive.h"
 #include "library/inductive_compiler/compiler.h"
diff --git a/src/library/init_module.cpp b/src/library/init_module.cpp
index 417d48099a..32a3510e5b 100644
--- a/src/library/init_module.cpp
+++ b/src/library/init_module.cpp
@@ -46,8 +46,6 @@ Author: Leonardo de Moura
 #include "library/mpq_macro.h"
 #include "library/arith_instance_manager.h"
 #include "library/inverse.h"
-#include "library/simp_lemmas.h"
-#include "library/eqn_lemmas.h"
 #include "library/pattern_attribute.h"
 
 namespace lean {
@@ -100,8 +98,6 @@ void initialize_library_module() {
     initialize_app_builder();
     initialize_fun_info();
     initialize_unification_hint();
-    initialize_simp_lemmas();
-    initialize_eqn_lemmas();
     initialize_type_context();
     initialize_delayed_abstraction();
     initialize_mpq_macro();
@@ -117,8 +113,6 @@ void finalize_library_module() {
     finalize_mpq_macro();
     finalize_delayed_abstraction();
     finalize_type_context();
-    finalize_eqn_lemmas();
-    finalize_simp_lemmas();
     finalize_unification_hint();
     finalize_fun_info();
     finalize_app_builder();
diff --git a/src/library/tactic/CMakeLists.txt b/src/library/tactic/CMakeLists.txt
index 5f01aa4928..6621e21ef5 100644
--- a/src/library/tactic/CMakeLists.txt
+++ b/src/library/tactic/CMakeLists.txt
@@ -6,4 +6,5 @@ add_library(tactic OBJECT occurrences.cpp kabstract.cpp tactic_state.cpp
   ac_tactics.cpp induction_tactic.cpp cases_tactic.cpp
   generalize_tactic.cpp rewrite_tactic.cpp unfold_tactic.cpp
   hsubstitution.cpp gexpr.cpp elaborate.cpp init_module.cpp
-  simp_result.cpp user_attribute.cpp eval.cpp simp_lemmas_tactics.cpp dsimplify.cpp)
+  simp_result.cpp user_attribute.cpp eval.cpp
+  simp_lemmas.cpp eqn_lemmas.cpp simp_lemmas_tactics.cpp dsimplify.cpp)
diff --git a/src/library/tactic/dsimplify.h b/src/library/tactic/dsimplify.h
index 1a0ec00504..51402b4aa9 100644
--- a/src/library/tactic/dsimplify.h
+++ b/src/library/tactic/dsimplify.h
@@ -6,7 +6,7 @@ Author: Leonardo de Moura
 */
 #pragma once
 #include "library/type_context.h"
-#include "library/simp_lemmas.h"
+#include "library/tactic/simp_lemmas.h"
 
 namespace lean {
 class dsimplify_core_fn {
diff --git a/src/library/eqn_lemmas.cpp b/src/library/tactic/eqn_lemmas.cpp
similarity index 98%
rename from src/library/eqn_lemmas.cpp
rename to src/library/tactic/eqn_lemmas.cpp
index 543aba7aa7..444131b1c8 100644
--- a/src/library/eqn_lemmas.cpp
+++ b/src/library/tactic/eqn_lemmas.cpp
@@ -8,9 +8,9 @@ Author: Leonardo de Moura
 #include "library/attribute_manager.h"
 #include "library/kernel_serializer.h"
 #include "library/trace.h"
-#include "library/eqn_lemmas.h"
 #include "library/constants.h"
 #include "library/module.h"
+#include "library/tactic/eqn_lemmas.h"
 
 namespace lean {
 struct eqn_lemmas_ext : public environment_extension {
diff --git a/src/library/eqn_lemmas.h b/src/library/tactic/eqn_lemmas.h
similarity index 92%
rename from src/library/eqn_lemmas.h
rename to src/library/tactic/eqn_lemmas.h
index 138e2f02fc..2cb3953a2c 100644
--- a/src/library/eqn_lemmas.h
+++ b/src/library/tactic/eqn_lemmas.h
@@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #pragma once
-#include "library/simp_lemmas.h"
+#include "library/tactic/simp_lemmas.h"
 
 namespace lean {
 environment add_eqn_lemma(environment const & env, name const & eqn_lemma);
diff --git a/src/library/tactic/init_module.cpp b/src/library/tactic/init_module.cpp
index 3fdf5569c3..a84aef2540 100644
--- a/src/library/tactic/init_module.cpp
+++ b/src/library/tactic/init_module.cpp
@@ -28,6 +28,8 @@ Author: Leonardo de Moura
 #include "library/tactic/elaborate.h"
 #include "library/tactic/user_attribute.h"
 #include "library/tactic/eval.h"
+#include "library/tactic/simp_lemmas.h"
+#include "library/tactic/eqn_lemmas.h"
 #include "library/tactic/simp_lemmas_tactics.h"
 #include "library/tactic/dsimplify.h"
 #include "library/tactic/simplifier/init_module.h"
@@ -61,11 +63,15 @@ void initialize_tactic_module() {
     initialize_elaborate();
     initialize_user_attribute();
     initialize_eval();
+    initialize_simp_lemmas();
+    initialize_eqn_lemmas();
     initialize_simp_lemmas_tactics();
     initialize_dsimplify();
 }
 void finalize_tactic_module() {
     finalize_dsimplify();
+    finalize_eqn_lemmas();
+    finalize_simp_lemmas();
     finalize_simp_lemmas_tactics();
     finalize_eval();
     finalize_user_attribute();
diff --git a/src/library/simp_lemmas.cpp b/src/library/tactic/simp_lemmas.cpp
similarity index 99%
rename from src/library/simp_lemmas.cpp
rename to src/library/tactic/simp_lemmas.cpp
index 047e5dcda5..b955564028 100644
--- a/src/library/simp_lemmas.cpp
+++ b/src/library/tactic/simp_lemmas.cpp
@@ -10,13 +10,13 @@ Author: Leonardo de Moura
 #include "kernel/instantiate.h"
 #include "kernel/for_each_fn.h"
 #include "kernel/find_fn.h"
-#include "library/simp_lemmas.h"
 #include "library/constants.h"
 #include "library/trace.h"
 #include "library/util.h"
 #include "library/reducible.h"
 #include "library/attribute_manager.h"
 #include "library/relation_manager.h"
+#include "library/tactic/simp_lemmas.h"
 
 namespace lean {
 LEAN_THREAD_VALUE(bool, g_throw_ex, false);
diff --git a/src/library/simp_lemmas.h b/src/library/tactic/simp_lemmas.h
similarity index 100%
rename from src/library/simp_lemmas.h
rename to src/library/tactic/simp_lemmas.h
diff --git a/src/library/tactic/simp_lemmas_tactics.cpp b/src/library/tactic/simp_lemmas_tactics.cpp
index 3ca2a4c7c7..1e28610df8 100644
--- a/src/library/tactic/simp_lemmas_tactics.cpp
+++ b/src/library/tactic/simp_lemmas_tactics.cpp
@@ -6,12 +6,12 @@ Author: Leonardo de Moura
 */
 #include "library/attribute_manager.h"
 #include "library/trace.h"
-#include "library/simp_lemmas.h"
 #include "library/constants.h"
 #include "library/vm/vm_expr.h"
 #include "library/vm/vm_list.h"
 #include "library/vm/vm_option.h"
 #include "library/vm/vm_name.h"
+#include "library/tactic/simp_lemmas.h"
 #include "library/tactic/simp_result.h"
 #include "library/tactic/tactic_state.h"
 
@@ -220,7 +220,7 @@ vm_obj simp_lemmas_rewrite(vm_obj const & m, vm_obj const & sls, vm_obj const &
                                     to_name(R), to_expr(e), to_tactic_state(s));
 }
 
-vm_obj simp_lemmas_drewrite_core(simp_lemmas const & sls, expr const & e, tactic_state const & s) {
+vm_obj simp_lemmas_drewrite_core(transparency_mode const & m, simp_lemmas const & sls, expr const & e, tactic_state const & s) {
     LEAN_TACTIC_TRY;
     simp_lemmas_for const * sr = sls.find(get_eq_name());
     if (!sr) return mk_tactic_exception("failed to apply simp_lemmas, no lemmas for 'eq' relation", s);
@@ -228,7 +228,7 @@ vm_obj simp_lemmas_drewrite_core(simp_lemmas const & sls, expr const & e, tactic
     list<simp_lemma> const * srs = sr->find(e);
     if (!srs) return mk_tactic_exception("failed to apply simp_lemmas, no simp lemma", s);
 
-    type_context ctx = mk_type_context_for(s);
+    type_context ctx = mk_type_context_for(s, m);
 
     for (simp_lemma const & lemma : *srs) {
         if (lemma.is_refl()) {
@@ -241,8 +241,8 @@ vm_obj simp_lemmas_drewrite_core(simp_lemmas const & sls, expr const & e, tactic
     LEAN_TACTIC_CATCH(s);
 }
 
-vm_obj simp_lemmas_drewrite(vm_obj const & sls, vm_obj const & e, vm_obj const & s) {
-    return simp_lemmas_drewrite_core(to_simp_lemmas(sls), to_expr(e), to_tactic_state(s));
+vm_obj simp_lemmas_drewrite(vm_obj const & m, vm_obj const & sls, vm_obj const & e, vm_obj const & s) {
+    return simp_lemmas_drewrite_core(to_transparency_mode(m), to_simp_lemmas(sls), to_expr(e), to_tactic_state(s));
 }
 
 void initialize_simp_lemmas_tactics() {
@@ -254,7 +254,7 @@ void initialize_simp_lemmas_tactics() {
     DECLARE_VM_BUILTIN(name({"simp_lemmas", "add_simp_core"}),   simp_lemmas_add_simp);
     DECLARE_VM_BUILTIN(name({"simp_lemmas", "add_congr_core"}),  simp_lemmas_add_congr);
     DECLARE_VM_BUILTIN(name({"simp_lemmas", "rewrite_core"}),    simp_lemmas_rewrite);
-    DECLARE_VM_BUILTIN(name({"simp_lemmas", "drewrite"}),        simp_lemmas_drewrite);
+    DECLARE_VM_BUILTIN(name({"simp_lemmas", "drewrite_core"}),   simp_lemmas_drewrite);
 }
 
 void finalize_simp_lemmas_tactics() {
diff --git a/src/library/tactic/simp_lemmas_tactics.h b/src/library/tactic/simp_lemmas_tactics.h
index 6715c47f0e..25c056b43e 100644
--- a/src/library/tactic/simp_lemmas_tactics.h
+++ b/src/library/tactic/simp_lemmas_tactics.h
@@ -5,8 +5,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #pragma once
-#include "library/simp_lemmas.h"
 #include "library/vm/vm.h"
+#include "library/tactic/simp_lemmas.h"
 namespace lean {
 simp_lemmas const & to_simp_lemmas(vm_obj const & o);
 vm_obj to_obj(simp_lemmas const & s);
diff --git a/src/library/tactic/simplifier/simplifier.cpp b/src/library/tactic/simplifier/simplifier.cpp
index fdbf484e29..d97d55c1da 100644
--- a/src/library/tactic/simplifier/simplifier.cpp
+++ b/src/library/tactic/simplifier/simplifier.cpp
@@ -28,7 +28,6 @@ Author: Daniel Selsam
 #include "library/relation_manager.h"
 #include "library/app_builder.h"
 #include "library/congr_lemma.h"
-#include "library/simp_lemmas.h"
 #include "library/fun_info.h"
 #include "library/vm/vm_expr.h"
 #include "library/vm/vm_list.h"
@@ -36,6 +35,7 @@ Author: Daniel Selsam
 #include "library/tactic/tactic_state.h"
 #include "library/tactic/ac_tactics.h"
 #include "library/tactic/app_builder_tactics.h"
+#include "library/tactic/simp_lemmas.h"
 #include "library/tactic/simp_lemmas_tactics.h"
 #include "library/tactic/simplifier/simplifier.h"
 #include "library/tactic/simplifier/theory_simplifier.h"
diff --git a/src/library/tactic/simplifier/simplifier.h b/src/library/tactic/simplifier/simplifier.h
index 710b3a6abc..db55b1254e 100644
--- a/src/library/tactic/simplifier/simplifier.h
+++ b/src/library/tactic/simplifier/simplifier.h
@@ -6,8 +6,8 @@ Author: Daniel Selsam
 #pragma once
 #include "kernel/expr_pair.h"
 #include "library/type_context.h"
-#include "library/simp_lemmas.h"
 #include "library/vm/vm.h"
+#include "library/tactic/simp_lemmas.h"
 #include "library/tactic/simp_result.h"
 
 namespace lean {
diff --git a/src/library/tactic/unfold_tactic.cpp b/src/library/tactic/unfold_tactic.cpp
index aa8b8729e5..8ff4bd1c0d 100644
--- a/src/library/tactic/unfold_tactic.cpp
+++ b/src/library/tactic/unfold_tactic.cpp
@@ -14,9 +14,9 @@ Author: Leonardo de Moura
 #include "library/replace_visitor.h"
 #include "library/constants.h"
 #include "library/user_recursors.h"
-#include "library/eqn_lemmas.h"
 #include "library/vm/vm_list.h"
 #include "library/vm/vm_expr.h"
+#include "library/tactic/eqn_lemmas.h"
 #include "library/tactic/tactic_state.h"
 #include "library/tactic/occurrences.h"