diff --git a/src/emacs/lean-syntax.el b/src/emacs/lean-syntax.el
index c20a69205..f337ddaee 100644
--- a/src/emacs/lean-syntax.el
+++ b/src/emacs/lean-syntax.el
@@ -118,7 +118,7 @@
      ;; modifiers
      (,(rx (or "\[persistent\]" "\[notation\]" "\[visible\]" "\[instance\]" "\[class\]" "\[parsing-only\]"
                "\[coercion\]" "\[reducible\]" "\[irreducible\]" "\[wf\]" "\[whnf\]" "\[multiple-instances\]"
-               "\[decls\]" "\[strict\]" "\[coercions\]" "\[classes\]" "\[notations\]" "\[tactic_hints\]" "\[reduce_hints\]"))
+               "\[decls\]" "\[all-transparent\]" "\[coercions\]" "\[classes\]" "\[notations\]" "\[tactic_hints\]" "\[reduce_hints\]"))
       . 'font-lock-doc-face)
      (,(rx "\[priority" (zero-or-more (not (any "\]"))) "\]") . font-lock-doc-face)
      (,(rx "\[unfold-c" (zero-or-more (not (any "\]"))) "\]") . font-lock-doc-face)
diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp
index 8f1e50222..5fd98f365 100644
--- a/src/frontends/lean/builtin_cmds.cpp
+++ b/src/frontends/lean/builtin_cmds.cpp
@@ -12,6 +12,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/io_state_stream.h"
 #include "library/scoped_ext.h"
 #include "library/aliases.h"
@@ -322,15 +323,25 @@ environment check_cmd(parser & p) {
     return p.env();
 }
 
+class all_transparent_converter : public default_converter {
+public:
+    all_transparent_converter(environment const & env):
+        default_converter(env, optional<module_idx>(), true) {
+    }
+    virtual bool is_opaque(declaration const &) const {
+        return false;
+    }
+};
+
 environment eval_cmd(parser & p) {
     bool whnf   = false;
-    bool strict = false;
+    bool all_transparent = false;
     if (p.curr_is_token(get_whnf_tk())) {
         p.next();
         whnf = true;
-    } else if (p.curr_is_token(get_strict_tk())) {
+    } else if (p.curr_is_token(get_all_transparent_tk())) {
         p.next();
-        strict = true;
+        all_transparent = true;
     }
     expr e; level_param_names ls;
     std::tie(e, ls) = parse_local_expr(p);
@@ -338,10 +349,11 @@ environment eval_cmd(parser & p) {
     if (whnf) {
         auto tc = mk_type_checker(p.env(), p.mk_ngen(), true);
         r = tc->whnf(e).first;
-    } else if (strict) {
-        r = normalize(p.env(), ls, e);
+    } else if (all_transparent) {
+        type_checker tc(p.env(), name_generator(),
+                        std::unique_ptr<converter>(new all_transparent_converter(p.env())));
+        r = normalize(tc, ls, e);
     } else {
-        transparent_scope scope;
         r = normalize(p.env(), ls, e);
     }
     flycheck_information info(p.regular_stream());
diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp
index 26cc65beb..9edaac331 100644
--- a/src/frontends/lean/token_table.cpp
+++ b/src/frontends/lean/token_table.cpp
@@ -90,7 +90,7 @@ void init_token_table(token_table & t) {
         {"theorem", "axiom", "variable", "protected", "private", "opaque", "definition", "example", "coercion",
          "variables", "parameter", "parameters", "constant", "constants", "[persistent]", "[visible]", "[instance]",
          "[off]", "[on]", "[none]", "[class]", "[coercion]", "[reducible]", "[irreducible]", "[parsing-only]", "[multiple-instances]",
-         "evaluate", "check", "eval", "[wf]", "[whnf]", "[strict]", "[priority", "[unfold-c", "print", "end", "namespace", "section", "prelude",
+         "evaluate", "check", "eval", "[wf]", "[whnf]", "[all-transparent]", "[priority", "[unfold-c", "print", "end", "namespace", "section", "prelude",
          "import", "inductive", "record", "structure", "module", "universe", "universes", "local",
          "precedence", "reserve", "infixl", "infixr", "infix", "postfix", "prefix", "notation", "context",
          "exit", "set_option", "open", "export", "calc_subst", "calc_refl", "calc_trans", "calc_symm", "tactic_hint",
diff --git a/src/frontends/lean/tokens.cpp b/src/frontends/lean/tokens.cpp
index a8af626f5..ddef8980d 100644
--- a/src/frontends/lean/tokens.cpp
+++ b/src/frontends/lean/tokens.cpp
@@ -71,7 +71,7 @@ static name * g_off          = nullptr;
 static name * g_none         = nullptr;
 static name * g_whnf         = nullptr;
 static name * g_wf           = nullptr;
-static name * g_strict       = nullptr;
+static name * g_all_transparent = nullptr;
 static name * g_in           = nullptr;
 static name * g_at           = nullptr;
 static name * g_assign       = nullptr;
@@ -187,7 +187,7 @@ void initialize_tokens() {
     g_none         = new name("[none]");
     g_whnf         = new name("[whnf]");
     g_wf           = new name("[wf]");
-    g_strict       = new name("[strict]");
+    g_all_transparent = new name("[all-transparent]");
     g_in           = new name("in");
     g_at           = new name("at");
     g_assign       = new name(":=");
@@ -309,7 +309,7 @@ void finalize_tokens() {
     delete g_none;
     delete g_whnf;
     delete g_wf;
-    delete g_strict;
+    delete g_all_transparent;
     delete g_ellipsis;
     delete g_fun;
     delete g_take;
@@ -420,7 +420,7 @@ name const & get_off_tk() { return *g_off; }
 name const & get_none_tk() { return *g_none; }
 name const & get_whnf_tk() { return *g_whnf; }
 name const & get_wf_tk() { return *g_wf; }
-name const & get_strict_tk() { return *g_strict; }
+name const & get_all_transparent_tk() { return *g_all_transparent; }
 name const & get_in_tk() { return *g_in; }
 name const & get_at_tk() { return *g_at; }
 name const & get_assign_tk() { return *g_assign; }
diff --git a/src/frontends/lean/tokens.h b/src/frontends/lean/tokens.h
index d7a2eb60f..0a30022a4 100644
--- a/src/frontends/lean/tokens.h
+++ b/src/frontends/lean/tokens.h
@@ -73,7 +73,7 @@ name const & get_off_tk();
 name const & get_none_tk();
 name const & get_whnf_tk();
 name const & get_wf_tk();
-name const & get_strict_tk();
+name const & get_all_transparent_tk();
 name const & get_in_tk();
 name const & get_at_tk();
 name const & get_assign_tk();
diff --git a/src/kernel/converter.cpp b/src/kernel/converter.cpp
index 50b528bcc..e3bf6b4b2 100644
--- a/src/kernel/converter.cpp
+++ b/src/kernel/converter.cpp
@@ -14,16 +14,6 @@ Author: Leonardo de Moura
 #include "kernel/default_converter.h"
 
 namespace lean {
-// Temporary hack for ignoring opaque annotations in the kernel
-LEAN_THREAD_VALUE(unsigned, g_everything_transparent, false);
-
-transparent_scope::transparent_scope():m_old_value(g_everything_transparent) {
-    g_everything_transparent = true;
-}
-transparent_scope::~transparent_scope() {
-    g_everything_transparent = m_old_value;
-}
-
 /**
    \brief Predicate for deciding whether \c d is an opaque definition or not.
 
@@ -46,7 +36,6 @@ transparent_scope::~transparent_scope() {
 */
 bool is_opaque(declaration const & d, extra_opaque_pred const & pred, optional<module_idx> const & mod_idx) {
     lean_assert(d.is_definition());
-    if (g_everything_transparent) return false; // temporary hack
     if (d.is_theorem()) return true;                               // theorems are always opaque
     if (pred(d.get_name())) return true;                           // extra_opaque predicate overrides opaque flag
     if (!d.is_opaque()) return false;                              // d is a transparent definition
diff --git a/src/kernel/converter.h b/src/kernel/converter.h
index a996778c4..4d59a0189 100644
--- a/src/kernel/converter.h
+++ b/src/kernel/converter.h
@@ -25,14 +25,6 @@ public:
     pair<bool, constraint_seq> is_def_eq(expr const & t, expr const & s, type_checker & c);
 };
 
-/** \brief Temporary hack for creating a scope where the opaque annotations are ignored in the kernel. */
-class transparent_scope {
-    bool m_old_value;
-public:
-    transparent_scope();
-    ~transparent_scope();
-};
-
 std::unique_ptr<converter> mk_dummy_converter();
 std::unique_ptr<converter> mk_default_converter(environment const & env, optional<module_idx> mod_idx = optional<module_idx>(),
                                                 bool memoize = true);
diff --git a/src/kernel/default_converter.cpp b/src/kernel/default_converter.cpp
index d8e1e1050..e45695366 100644
--- a/src/kernel/default_converter.cpp
+++ b/src/kernel/default_converter.cpp
@@ -21,6 +21,9 @@ default_converter::default_converter(environment const & env, optional<module_id
     m_jst = nullptr;
 }
 
+default_converter::default_converter(environment const & env, optional<module_idx> mod_idx, bool memoize):
+    default_converter(env, mod_idx, memoize, [](name const &) { return false; }) {}
+
 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));
 }
@@ -105,19 +108,20 @@ expr default_converter::whnf_core(expr const & e) {
     return r;
 }
 
-bool default_converter::is_opaque_core(declaration const & d) const {
-    return ::lean::is_opaque(d, m_extra_pred, m_module_idx);
-}
-
 bool default_converter::is_opaque(declaration const & d) const {
-    return is_opaque_core(d);
+    lean_assert(d.is_definition());
+    if (d.is_theorem()) return true;                               // theorems are always opaque
+    if (m_extra_pred(d.get_name())) return true;                   // extra_opaque predicate overrides opaque flag
+    if (!d.is_opaque()) return false;                              // d is a transparent definition
+    if (m_module_idx && d.get_module_idx() == *m_module_idx) return false; // the opaque definitions in mod_idx are considered transparent
+    return true;                                                   // d is opaque
 }
 
 /** \brief Expand \c e if it is non-opaque constant with weight >= w */
 expr default_converter::unfold_name_core(expr e, unsigned w) {
     if (is_constant(e)) {
         if (auto d = m_env.find(const_name(e))) {
-            if (d->is_definition() && !is_opaque_core(*d) && d->get_weight() >= w)
+            if (d->is_definition() && !is_opaque(*d) && d->get_weight() >= w)
                 return unfold_name_core(instantiate_value_univ_params(*d, const_levels(e)), w);
         }
     }
@@ -472,7 +476,7 @@ pair<bool, constraint_seq> default_converter::is_def_eq(expr const & t, expr con
                         // If they are, then t_n and s_n must be definitionally equal, and we can
                         // skip the delta-reduction step.
                         // If the flag use_conv_opt() is not true, then we skip this optimization
-                        if (!is_opaque_core(*d_t) && d_t->use_conv_opt() &&
+                        if (!is_opaque(*d_t) && d_t->use_conv_opt() &&
                             is_def_eq_args(t_n, s_n, cs))
                             return to_bcs(true, cs);
                     }
diff --git a/src/kernel/default_converter.h b/src/kernel/default_converter.h
index 27a627ea7..235381ccf 100644
--- a/src/kernel/default_converter.h
+++ b/src/kernel/default_converter.h
@@ -35,7 +35,6 @@ protected:
     optional<pair<expr, constraint_seq>> norm_ext(expr const & e);
     optional<expr> d_norm_ext(expr const & e, constraint_seq & cs);
     expr whnf_core(expr const & e);
-    bool is_opaque_core(declaration const & d) const;
     expr unfold_name_core(expr e, unsigned w);
     expr unfold_names(expr const & e, unsigned w);
     optional<declaration> is_delta(expr const & e);
@@ -75,6 +74,7 @@ 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);
 
     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/normalize.cpp b/src/library/normalize.cpp
index 1486f140b..dfdae341b 100644
--- a/src/library/normalize.cpp
+++ b/src/library/normalize.cpp
@@ -199,6 +199,11 @@ expr normalize(type_checker & tc, expr const & e) {
     return normalize_fn(tc, save_cnstrs)(e);
 }
 
+expr normalize(type_checker & tc, level_param_names const & ls, expr const & e) {
+    bool save_cnstrs = false;
+    return normalize_fn(tc, save_cnstrs)(ls, e);
+}
+
 expr normalize(type_checker & tc, expr const & e, constraint_seq & cs) {
     normalize_fn fn(tc);
     expr r = fn(e);
diff --git a/src/library/normalize.h b/src/library/normalize.h
index afed47253..00a447b6d 100644
--- a/src/library/normalize.h
+++ b/src/library/normalize.h
@@ -19,6 +19,7 @@ expr normalize(environment const & env, level_param_names const & ls, expr const
 /** \brief Similar to <tt>expr normalize(environment const & env, expr const & e)</tt>, but
     uses the converter associated with \c tc. */
 expr normalize(type_checker & tc, expr const & e);
+expr normalize(type_checker & tc, level_param_names const & ls, expr const & e);
 /** \brief Return the \c e normal form with respect to \c tc, and store generated constraints
     into \c cs.
 */
diff --git a/tests/lean/eta_bug.lean b/tests/lean/eta_bug.lean
index c376ac032..9db364535 100644
--- a/tests/lean/eta_bug.lean
+++ b/tests/lean/eta_bug.lean
@@ -1,4 +1,4 @@
 import logic
-eval λ (A : Type) (x y : A) (H₁ : x = y) (H₂ : y = x), eq.trans H₁ H₂
+eval [all-transparent] λ (A : Type) (x y : A) (H₁ : x = y) (H₂ : y = x), eq.trans H₁ H₂
 -- Should not reduce to
 -- λ (A : Type) (x y : A), eq.trans