diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index 7d3e8326f..daa9ac3d3 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -1941,7 +1941,7 @@ class parser::imp {
         next();
         expr v = m_elaborator(parse_expr());
         normalizer norm(m_env);
-        expr r = norm(v);
+        expr r = norm(v, context(), true);
         regular(m_io_state) << r << endl;
     }
 
diff --git a/src/kernel/builtin.cpp b/src/kernel/builtin.cpp
index e4bcc8ad8..d9903bf84 100644
--- a/src/kernel/builtin.cpp
+++ b/src/kernel/builtin.cpp
@@ -235,22 +235,22 @@ void import_basic(environment const & env) {
     env->add_builtin(mk_if_fn());
 
     // implies(x, y) := if x y True
-    env->add_definition(implies_fn_name, p2, Fun({{x, Bool}, {y, Bool}}, bIf(x, y, True)));
+    env->add_opaque_definition(implies_fn_name, p2, Fun({{x, Bool}, {y, Bool}}, bIf(x, y, True)));
 
     // iff(x, y) := x = y
-    env->add_definition(iff_fn_name, p2, Fun({{x, Bool}, {y, Bool}}, Eq(x, y)));
+    env->add_opaque_definition(iff_fn_name, p2, Fun({{x, Bool}, {y, Bool}}, Eq(x, y)));
 
     // not(x) := if x False True
-    env->add_definition(not_fn_name, p1, Fun({x, Bool}, bIf(x, False, True)));
+    env->add_opaque_definition(not_fn_name, p1, Fun({x, Bool}, bIf(x, False, True)));
 
     // or(x, y) := Not(x) => y
-    env->add_definition(or_fn_name, p2, Fun({{x, Bool}, {y, Bool}}, Implies(Not(x), y)));
+    env->add_opaque_definition(or_fn_name, p2, Fun({{x, Bool}, {y, Bool}}, Implies(Not(x), y)));
 
     // and(x, y) := Not(x => Not(y))
-    env->add_definition(and_fn_name, p2, Fun({{x, Bool}, {y, Bool}}, Not(Implies(x, Not(y)))));
+    env->add_opaque_definition(and_fn_name, p2, Fun({{x, Bool}, {y, Bool}}, Not(Implies(x, Not(y)))));
 
     // forall : Pi (A : Type u), (A -> Bool) -> Bool
-    env->add_definition(forall_fn_name, q_type, Fun({{A, TypeU}, {P, A_pred}}, Eq(P, Fun({x, A}, True))));
+    env->add_opaque_definition(forall_fn_name, q_type, Fun({{A, TypeU}, {P, A_pred}}, Eq(P, Fun({x, A}, True))));
     // TODO(Leo): introduce epsilon
     env->add_definition(exists_fn_name, q_type, Fun({{A, TypeU}, {P, A_pred}}, Not(Forall(A, Fun({x, A}, Not(P(x)))))));
 
diff --git a/src/kernel/environment.cpp b/src/kernel/environment.cpp
index 1f8391afe..0e71ab030 100644
--- a/src/kernel/environment.cpp
+++ b/src/kernel/environment.cpp
@@ -397,8 +397,8 @@ expr environment_cell::infer_type(expr const & e, context const & ctx) const {
     return m_type_checker->infer_type(e, ctx);
 }
 
-expr environment_cell::normalize(expr const & e, context const & ctx) const {
-    return m_type_checker->get_normalizer()(e, ctx);
+expr environment_cell::normalize(expr const & e, context const & ctx, bool unfold_opaque) const {
+    return m_type_checker->get_normalizer()(e, ctx, unfold_opaque);
 }
 
 /** \brief Display universal variable constraints and objects stored in this environment and its parents. */
diff --git a/src/kernel/environment.h b/src/kernel/environment.h
index 652cecca8..3cd013e64 100644
--- a/src/kernel/environment.h
+++ b/src/kernel/environment.h
@@ -152,15 +152,14 @@ public:
        \brief Add a new definition n : t := v.
        It throws an exception if v does not have type t.
        It throws an exception if there is already an object with the given name.
-       If opaque == true, then definition is not used by normalizer.
     */
     void add_definition(name const & n, expr const & t, expr const & v, bool opaque = false);
+    void add_opaque_definition(name const & n, expr const & t, expr const & v) { add_definition(n, t, v, true); }
     void add_theorem(name const & n, expr const & t, expr const & v);
 
     /**
        \brief Add a new definition n : infer_type(v) := v.
        It throws an exception if there is already an object with the given name.
-       If opaque == true, then definition is not used by normalizer.
     */
     void add_definition(name const & n, expr const & v, bool opaque = false);
 
@@ -207,7 +206,7 @@ public:
     /**
        \brief Normalize \c e in the given context and this environment.
     */
-    expr normalize(expr const & e, context const & ctx = context()) const;
+    expr normalize(expr const & e, context const & ctx = context(), bool unfold_opaque = false) const;
 
     /**
        \brief Low-level function for accessing objects. Consider using iterators.
diff --git a/src/kernel/normalizer.cpp b/src/kernel/normalizer.cpp
index d2043f2cc..6d95be471 100644
--- a/src/kernel/normalizer.cpp
+++ b/src/kernel/normalizer.cpp
@@ -79,6 +79,7 @@ class normalizer::imp {
     context                  m_ctx;
     cached_metavar_env       m_menv;
     cache                    m_cache;
+    bool                     m_unfold_opaque;
     unsigned                 m_max_depth;
     unsigned                 m_depth;
 
@@ -201,7 +202,7 @@ class normalizer::imp {
             break;
         case expr_kind::Constant: {
             object const & obj = env()->get_object(const_name(a));
-            if (obj.is_definition() && !obj.is_opaque()) {
+            if (should_unfold(obj, m_unfold_opaque)) {
                 freset<cache> reset(m_cache);
                 r = normalize(obj.get_value(), value_stack(), 0);
             } else {
@@ -291,9 +292,13 @@ public:
         m_env(env) {
         m_max_depth      = max_depth;
         m_depth          = 0;
+        m_unfold_opaque  = false;
     }
 
-    expr operator()(expr const & e, context const & ctx, optional<metavar_env> const & menv) {
+    expr operator()(expr const & e, context const & ctx, optional<metavar_env> const & menv, bool unfold_opaque) {
+        if (m_unfold_opaque != unfold_opaque)
+            m_cache.clear();
+        m_unfold_opaque = unfold_opaque;
         set_ctx(ctx);
         if (m_menv.update(menv))
             m_cache.clear();
@@ -308,13 +313,19 @@ normalizer::normalizer(ro_environment const & env, unsigned max_depth):m_ptr(new
 normalizer::normalizer(ro_environment const & env):normalizer(env, std::numeric_limits<unsigned>::max()) {}
 normalizer::normalizer(ro_environment const & env, options const & opts):normalizer(env, get_normalizer_max_depth(opts)) {}
 normalizer::~normalizer() {}
-expr normalizer::operator()(expr const & e, context const & ctx, optional<metavar_env> const & menv) { return (*m_ptr)(e, ctx, menv); }
-expr normalizer::operator()(expr const & e, context const & ctx, metavar_env const & menv) { return operator()(e, ctx, some_menv(menv)); }
-expr normalizer::operator()(expr const & e, context const & ctx) { return operator()(e, ctx, none_menv()); }
+expr normalizer::operator()(expr const & e, context const & ctx, optional<metavar_env> const & menv, bool unfold_opaque) {
+    return (*m_ptr)(e, ctx, menv, unfold_opaque);
+}
+expr normalizer::operator()(expr const & e, context const & ctx, metavar_env const & menv, bool unfold_opaque) {
+    return operator()(e, ctx, some_menv(menv), unfold_opaque);
+}
+expr normalizer::operator()(expr const & e, context const & ctx, bool unfold_opaque) {
+    return operator()(e, ctx, none_menv(), unfold_opaque);
+}
 void normalizer::clear() { m_ptr->clear(); }
 
-expr normalize(expr const & e, ro_environment const & env, context const & ctx) {
-    return normalizer(env)(e, ctx);
+expr normalize(expr const & e, ro_environment const & env, context const & ctx, bool unfold_opaque) {
+    return normalizer(env)(e, ctx, unfold_opaque);
 }
 }
 
diff --git a/src/kernel/normalizer.h b/src/kernel/normalizer.h
index 25310a264..ebbc46fa7 100644
--- a/src/kernel/normalizer.h
+++ b/src/kernel/normalizer.h
@@ -24,12 +24,12 @@ public:
     normalizer(ro_environment const & env, options const & opts);
     ~normalizer();
 
-    expr operator()(expr const & e, context const & ctx, optional<metavar_env> const & menv);
-    expr operator()(expr const & e, context const & ctx, metavar_env const & menv);
-    expr operator()(expr const & e, context const & ctx = context());
+    expr operator()(expr const & e, context const & ctx, optional<metavar_env> const & menv, bool unfold_opaque = false);
+    expr operator()(expr const & e, context const & ctx, metavar_env const & menv, bool unfold_opaque = false);
+    expr operator()(expr const & e, context const & ctx = context(), bool unfold_opaque = false);
 
     void clear();
 };
 /** \brief Normalize \c e using the environment \c env and context \c ctx */
-expr normalize(expr const & e, ro_environment const & env, context const & ctx = context());
+expr normalize(expr const & e, ro_environment const & env, context const & ctx = context(), bool unfold_opaque = false);
 }
diff --git a/src/kernel/object.h b/src/kernel/object.h
index 033e952dd..863438cf6 100644
--- a/src/kernel/object.h
+++ b/src/kernel/object.h
@@ -145,4 +145,21 @@ object mk_theorem(name const & n, expr const & t, expr const & v);
 object mk_axiom(name const & n, expr const & t);
 object mk_var_decl(name const & n, expr const & t);
 inline object mk_neutral(neutral_object_cell * c) { lean_assert(c->get_rc() == 1); return object(c); }
+
+/**
+   \brief Helper function whether we should unfold an definition or not.
+
+   1- We unfold definitions.
+   2- We never unfold theorems.
+   3- We unfold opaque definitions if \c unfold_opaque == true
+*/
+inline bool should_unfold(object const & obj, bool unfold_opaque) {
+    return obj.is_definition() && !obj.is_theorem() && (unfold_opaque || !obj.is_opaque());
+}
+inline bool should_unfold(optional<object> const & obj, bool unfold_opaque) {
+    return obj && should_unfold(*obj, unfold_opaque);
+}
+inline bool should_unfold(optional<object> const & obj) {
+    return should_unfold(obj, false);
+}
 }
diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp
index 5e6736742..273d06345 100644
--- a/src/kernel/type_checker.cpp
+++ b/src/kernel/type_checker.cpp
@@ -51,14 +51,14 @@ class type_checker::imp {
         return ::lean::instantiate(e, v, m_menv.to_some_menv());
     }
 
-    expr normalize(expr const & e, context const & ctx) {
-        return m_normalizer(e, ctx, m_menv.to_some_menv());
+    expr normalize(expr const & e, context const & ctx, bool unfold_opaque) {
+        return m_normalizer(e, ctx, m_menv.to_some_menv(), unfold_opaque);
     }
 
     expr check_pi(expr const & e, expr const & s, context const & ctx) {
         if (is_pi(e))
             return e;
-        expr r = normalize(e, ctx);
+        expr r = normalize(e, ctx, false);
         if (is_pi(r))
             return r;
         if (has_metavar(r) && m_menv && m_uc) {
@@ -71,6 +71,9 @@ class type_checker::imp {
             m_uc->push_back(mk_eq_constraint(ctx, e, p, jst));
             return p;
         }
+        r = normalize(e, ctx, true);
+        if (is_pi(r))
+            return r;
         throw function_expected_exception(env(), ctx, s);
     }
 
@@ -79,7 +82,7 @@ class type_checker::imp {
             return e;
         if (is_bool(e))
             return Type();
-        expr u = normalize(e, ctx);
+        expr u = normalize(e, ctx, false);
         if (is_type(u))
             return u;
         if (is_bool(u))
@@ -89,6 +92,11 @@ class type_checker::imp {
             m_uc->push_back(mk_convertible_constraint(ctx, e, TypeU, jst));
             return u;
         }
+        u = normalize(e, ctx, true);
+        if (is_type(u))
+            return u;
+        if (is_bool(u))
+            return Type();
         throw type_expected_exception(env(), ctx, s);
     }
 
@@ -267,18 +275,21 @@ class type_checker::imp {
     bool is_convertible(expr const & given, expr const & expected, context const & ctx, MkJustification const & mk_justification) {
         if (is_convertible_core(given, expected))
             return true;
-        expr new_given    = normalize(given, ctx);
-        expr new_expected = normalize(expected, ctx);
+        expr new_given    = normalize(given, ctx, false);
+        expr new_expected = normalize(expected, ctx, false);
         if (is_convertible_core(new_given, new_expected))
             return true;
         if (m_menv && m_uc && (has_metavar(new_given) || has_metavar(new_expected))) {
             m_uc->push_back(mk_convertible_constraint(ctx, given, expected, mk_justification()));
             return true;
         }
+        new_given    = normalize(new_given, ctx, true);
+        new_expected = normalize(new_expected, ctx, true);
+        if (is_convertible_core(new_given, new_expected))
+            return true;
         return false;
     }
 
-
     void set_ctx(context const & ctx) {
         if (!is_eqp(m_ctx, ctx)) {
             clear();
diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt
index 741900bc7..4c5502ea3 100644
--- a/src/library/CMakeLists.txt
+++ b/src/library/CMakeLists.txt
@@ -1,6 +1,6 @@
 add_library(library kernel_bindings.cpp basic_thms.cpp deep_copy.cpp
   max_sharing.cpp context_to_lambda.cpp io_state.cpp type_inferer.cpp
-  placeholder.cpp expr_lt.cpp hidden_defs.cpp substitution.cpp
+  placeholder.cpp expr_lt.cpp substitution.cpp
   fo_unify.cpp)
 
 target_link_libraries(library ${LEAN_LIBS})
diff --git a/src/library/all/all.cpp b/src/library/all/all.cpp
index 4fd71f7e3..d19c4711c 100644
--- a/src/library/all/all.cpp
+++ b/src/library/all/all.cpp
@@ -5,7 +5,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include "kernel/builtin.h"
-#include "library/hidden_defs.h"
 #include "library/basic_thms.h"
 #include "library/arith/arith.h"
 #include "library/cast/cast.h"
@@ -14,7 +13,6 @@ Author: Leonardo de Moura
 namespace lean {
 void import_all(environment const & env) {
     import_basic(env);
-    hide_builtin(env);
     import_basic_thms(env);
     import_cast(env);
     import_arith(env);
diff --git a/src/library/arith/int.cpp b/src/library/arith/int.cpp
index f2900a5f1..ac935276f 100644
--- a/src/library/arith/int.cpp
+++ b/src/library/arith/int.cpp
@@ -6,7 +6,6 @@ Author: Leonardo de Moura
 */
 #include "kernel/abstract.h"
 #include "kernel/environment.h"
-#include "library/hidden_defs.h"
 #include "library/kernel_bindings.h"
 #include "library/arith/int.h"
 #include "library/arith/nat.h"
@@ -162,23 +161,17 @@ void import_int(environment const & env) {
     env->add_builtin(mk_int_le_fn());
     env->add_builtin(mk_nat_to_int_fn());
 
-    env->add_definition(int_sub_fn_name, ii_i, Fun({{x, Int}, {y, Int}}, iAdd(x, iMul(iVal(-1), y))));
-    env->add_definition(int_neg_fn_name, i_i, Fun({x, Int}, iMul(iVal(-1), x)));
-    env->add_definition(int_mod_fn_name, ii_i, Fun({{x, Int}, {y, Int}}, iSub(x, iMul(y, iDiv(x, y)))));
-    env->add_definition(int_divides_fn_name, ii_b, Fun({{x, Int}, {y, Int}}, Eq(iMod(y, x), iVal(0))));
-    env->add_definition(int_ge_fn_name, ii_b,  Fun({{x, Int}, {y, Int}}, iLe(y, x)));
-    env->add_definition(int_lt_fn_name, ii_b,  Fun({{x, Int}, {y, Int}}, Not(iLe(y, x))));
-    env->add_definition(int_gt_fn_name, ii_b,  Fun({{x, Int}, {y, Int}}, Not(iLe(x, y))));
-    env->add_definition(int_abs_fn_name, i_i, Fun({x, Int}, iIf(iLe(iVal(0), x), x, iNeg(x))));
+    env->add_opaque_definition(int_sub_fn_name, ii_i, Fun({{x, Int}, {y, Int}}, iAdd(x, iMul(iVal(-1), y))));
+    env->add_opaque_definition(int_neg_fn_name, i_i, Fun({x, Int}, iMul(iVal(-1), x)));
+    env->add_opaque_definition(int_mod_fn_name, ii_i, Fun({{x, Int}, {y, Int}}, iSub(x, iMul(y, iDiv(x, y)))));
+    env->add_opaque_definition(int_divides_fn_name, ii_b, Fun({{x, Int}, {y, Int}}, Eq(iMod(y, x), iVal(0))));
+    env->add_opaque_definition(int_ge_fn_name, ii_b,  Fun({{x, Int}, {y, Int}}, iLe(y, x)));
+    env->add_opaque_definition(int_lt_fn_name, ii_b,  Fun({{x, Int}, {y, Int}}, Not(iLe(y, x))));
+    env->add_opaque_definition(int_gt_fn_name, ii_b,  Fun({{x, Int}, {y, Int}}, Not(iLe(x, y))));
+    env->add_opaque_definition(int_abs_fn_name, i_i, Fun({x, Int}, iIf(iLe(iVal(0), x), x, iNeg(x))));
 
-    env->add_definition(nat_sub_fn_name, Nat >> (Nat >> Int), Fun({{x, Nat}, {y, Nat}}, iSub(n2i(x), n2i(y))));
-    env->add_definition(nat_neg_fn_name, Nat >> Int, Fun({x, Nat}, iNeg(n2i(x))));
-
-    for (auto n : {int_sub_fn_name, int_neg_fn_name, int_mod_fn_name, int_divides_fn_name,
-                int_ge_fn_name, int_lt_fn_name, int_gt_fn_name, int_abs_fn_name,
-                nat_sub_fn_name, nat_neg_fn_name}) {
-        set_hidden_flag(env, n);
-    }
+    env->add_opaque_definition(nat_sub_fn_name, Nat >> (Nat >> Int), Fun({{x, Nat}, {y, Nat}}, iSub(n2i(x), n2i(y))));
+    env->add_opaque_definition(nat_neg_fn_name, Nat >> Int, Fun({x, Nat}, iNeg(n2i(x))));
 }
 
 static int mk_int_value(lua_State * L) {
diff --git a/src/library/arith/nat.cpp b/src/library/arith/nat.cpp
index 3e10f6a8a..0d0928c83 100644
--- a/src/library/arith/nat.cpp
+++ b/src/library/arith/nat.cpp
@@ -6,7 +6,6 @@ Author: Leonardo de Moura
 */
 #include "kernel/abstract.h"
 #include "kernel/environment.h"
-#include "library/hidden_defs.h"
 #include "library/kernel_bindings.h"
 #include "library/arith/nat.h"
 #include "library/arith/num_type.h"
@@ -122,14 +121,10 @@ void import_nat(environment const & env) {
     env->add_builtin(mk_nat_mul_fn());
     env->add_builtin(mk_nat_le_fn());
 
-    env->add_definition(nat_ge_fn_name, nn_b, Fun({{x, Nat}, {y, Nat}}, nLe(y, x)));
-    env->add_definition(nat_lt_fn_name, nn_b, Fun({{x, Nat}, {y, Nat}}, Not(nLe(y, x))));
-    env->add_definition(nat_gt_fn_name, nn_b, Fun({{x, Nat}, {y, Nat}}, Not(nLe(x, y))));
-    env->add_definition(nat_id_fn_name, Nat >> Nat, Fun({x, Nat}, x));
-
-    for (auto n : {nat_ge_fn_name, nat_lt_fn_name, nat_gt_fn_name, nat_id_fn_name}) {
-        set_hidden_flag(env, n);
-    }
+    env->add_opaque_definition(nat_ge_fn_name, nn_b, Fun({{x, Nat}, {y, Nat}}, nLe(y, x)));
+    env->add_opaque_definition(nat_lt_fn_name, nn_b, Fun({{x, Nat}, {y, Nat}}, Not(nLe(y, x))));
+    env->add_opaque_definition(nat_gt_fn_name, nn_b, Fun({{x, Nat}, {y, Nat}}, Not(nLe(x, y))));
+    env->add_opaque_definition(nat_id_fn_name, Nat >> Nat, Fun({x, Nat}, x));
 }
 
 static int mk_nat_value(lua_State * L) {
diff --git a/src/library/arith/real.cpp b/src/library/arith/real.cpp
index 5c2b08a8c..2e136608f 100644
--- a/src/library/arith/real.cpp
+++ b/src/library/arith/real.cpp
@@ -6,7 +6,6 @@ Author: Leonardo de Moura
 */
 #include "kernel/abstract.h"
 #include "kernel/environment.h"
-#include "library/hidden_defs.h"
 #include "library/kernel_bindings.h"
 #include "library/arith/real.h"
 #include "library/arith/int.h"
@@ -149,17 +148,12 @@ void import_real(environment const & env) {
     env->add_builtin(mk_real_div_fn());
     env->add_builtin(mk_real_le_fn());
 
-    env->add_definition(real_sub_fn_name, rr_r, Fun({{x, Real}, {y, Real}}, rAdd(x, rMul(rVal(-1), y))));
-    env->add_definition(real_neg_fn_name, r_r,  Fun({x, Real}, rMul(rVal(-1), x)));
-    env->add_definition(real_abs_fn_name, r_r,  Fun({x, Real}, rIf(rLe(rVal(0), x), x, rNeg(x))));
-    env->add_definition(real_ge_fn_name, rr_b,  Fun({{x, Real}, {y, Real}}, rLe(y, x)));
-    env->add_definition(real_lt_fn_name, rr_b,  Fun({{x, Real}, {y, Real}}, Not(rLe(y, x))));
-    env->add_definition(real_gt_fn_name, rr_b,  Fun({{x, Real}, {y, Real}}, Not(rLe(x, y))));
-
-    for (auto n : {real_sub_fn_name, real_neg_fn_name, real_abs_fn_name, real_ge_fn_name,
-                real_lt_fn_name, real_gt_fn_name}) {
-        set_hidden_flag(env, n);
-    }
+    env->add_opaque_definition(real_sub_fn_name, rr_r, Fun({{x, Real}, {y, Real}}, rAdd(x, rMul(rVal(-1), y))));
+    env->add_opaque_definition(real_neg_fn_name, r_r,  Fun({x, Real}, rMul(rVal(-1), x)));
+    env->add_opaque_definition(real_abs_fn_name, r_r,  Fun({x, Real}, rIf(rLe(rVal(0), x), x, rNeg(x))));
+    env->add_opaque_definition(real_ge_fn_name, rr_b,  Fun({{x, Real}, {y, Real}}, rLe(y, x)));
+    env->add_opaque_definition(real_lt_fn_name, rr_b,  Fun({{x, Real}, {y, Real}}, Not(rLe(y, x))));
+    env->add_opaque_definition(real_gt_fn_name, rr_b,  Fun({{x, Real}, {y, Real}}, Not(rLe(x, y))));
 }
 
 class int_to_real_value : public const_value {
@@ -184,9 +178,7 @@ void import_int_to_real_coercions(environment const & env) {
 
     env->add_builtin(mk_int_to_real_fn());
     expr x    = Const("x");
-    env->add_definition(nat_to_real_fn_name, Nat >> Real, Fun({x, Nat}, i2r(n2i(x))));
-
-    set_hidden_flag(env, nat_to_real_fn_name);
+    env->add_opaque_definition(nat_to_real_fn_name, Nat >> Real, Fun({x, Nat}, i2r(n2i(x))));
 }
 
 static int mk_real_value(lua_State * L) {
diff --git a/src/library/arith/special_fn.cpp b/src/library/arith/special_fn.cpp
index a111673ad..8dbed647b 100644
--- a/src/library/arith/special_fn.cpp
+++ b/src/library/arith/special_fn.cpp
@@ -6,7 +6,6 @@ Author: Leonardo de Moura
 */
 #include "kernel/environment.h"
 #include "kernel/abstract.h"
-#include "library/hidden_defs.h"
 #include "library/arith/special_fn.h"
 #include "library/arith/real.h"
 
@@ -43,24 +42,19 @@ void import_special_fn(environment const & env) {
     env->add_var(real_pi_name, Real);
     env->add_definition(name("pi"), Real, mk_real_pi()); // alias for pi
     env->add_var(sin_fn_name, r_r);
-    env->add_definition(cos_fn_name, r_r, Fun({x, Real}, Sin(rSub(x, rDiv(mk_real_pi(), rVal(2))))));
-    env->add_definition(tan_fn_name, r_r, Fun({x, Real}, rDiv(Sin(x), Cos(x))));
-    env->add_definition(cot_fn_name, r_r, Fun({x, Real}, rDiv(Cos(x), Sin(x))));
-    env->add_definition(sec_fn_name, r_r, Fun({x, Real}, rDiv(rVal(1), Cos(x))));
-    env->add_definition(csc_fn_name, r_r, Fun({x, Real}, rDiv(rVal(1), Sin(x))));
+    env->add_opaque_definition(cos_fn_name, r_r, Fun({x, Real}, Sin(rSub(x, rDiv(mk_real_pi(), rVal(2))))));
+    env->add_opaque_definition(tan_fn_name, r_r, Fun({x, Real}, rDiv(Sin(x), Cos(x))));
+    env->add_opaque_definition(cot_fn_name, r_r, Fun({x, Real}, rDiv(Cos(x), Sin(x))));
+    env->add_opaque_definition(sec_fn_name, r_r, Fun({x, Real}, rDiv(rVal(1), Cos(x))));
+    env->add_opaque_definition(csc_fn_name, r_r, Fun({x, Real}, rDiv(rVal(1), Sin(x))));
 
-    env->add_definition(sinh_fn_name, r_r, Fun({x, Real}, rDiv(rSub(rVal(1), Exp(rMul(rVal(-2), x))),
+    env->add_opaque_definition(sinh_fn_name, r_r, Fun({x, Real}, rDiv(rSub(rVal(1), Exp(rMul(rVal(-2), x))),
                                                               rMul(rVal(2), Exp(rNeg(x))))));
-    env->add_definition(cosh_fn_name, r_r, Fun({x, Real}, rDiv(rAdd(rVal(1), Exp(rMul(rVal(-2), x))),
+    env->add_opaque_definition(cosh_fn_name, r_r, Fun({x, Real}, rDiv(rAdd(rVal(1), Exp(rMul(rVal(-2), x))),
                                                               rMul(rVal(2), Exp(rNeg(x))))));
-    env->add_definition(tanh_fn_name, r_r, Fun({x, Real}, rDiv(Sinh(x), Cosh(x))));
-    env->add_definition(coth_fn_name, r_r, Fun({x, Real}, rDiv(Cosh(x), Sinh(x))));
-    env->add_definition(sech_fn_name, r_r, Fun({x, Real}, rDiv(rVal(1), Cosh(x))));
-    env->add_definition(csch_fn_name, r_r, Fun({x, Real}, rDiv(rVal(1), Sinh(x))));
-
-    for (auto n : {cos_fn_name, tan_fn_name, cot_fn_name, sec_fn_name, csc_fn_name, sinh_fn_name,
-                cosh_fn_name, tanh_fn_name, coth_fn_name, sech_fn_name, csch_fn_name}) {
-        set_hidden_flag(env, n);
-    }
+    env->add_opaque_definition(tanh_fn_name, r_r, Fun({x, Real}, rDiv(Sinh(x), Cosh(x))));
+    env->add_opaque_definition(coth_fn_name, r_r, Fun({x, Real}, rDiv(Cosh(x), Sinh(x))));
+    env->add_opaque_definition(sech_fn_name, r_r, Fun({x, Real}, rDiv(rVal(1), Cosh(x))));
+    env->add_opaque_definition(csch_fn_name, r_r, Fun({x, Real}, rDiv(rVal(1), Sinh(x))));
 }
 }
diff --git a/src/library/elaborator/elaborator.cpp b/src/library/elaborator/elaborator.cpp
index 4efea6f37..c348036f8 100644
--- a/src/library/elaborator/elaborator.cpp
+++ b/src/library/elaborator/elaborator.cpp
@@ -19,7 +19,6 @@ Author: Leonardo de Moura
 #include "kernel/replace_fn.h"
 #include "kernel/builtin.h"
 #include "kernel/update_expr.h"
-#include "library/hidden_defs.h"
 #include "library/type_inferer.h"
 #include "library/elaborator/elaborator.h"
 #include "library/elaborator/elaborator_justification.h"
@@ -627,7 +626,7 @@ class elaborator::imp {
     int get_const_weight(expr const & a) {
         lean_assert(is_constant(a));
         optional<object> obj = m_env->find_object(const_name(a));
-        if (obj && obj->is_definition() && !obj->is_opaque() && !is_hidden(m_env, const_name(a)))
+        if (should_unfold(obj))
             return obj->get_weight();
         else
             return -1;
diff --git a/src/library/hidden_defs.cpp b/src/library/hidden_defs.cpp
deleted file mode 100644
index 28180f9fe..000000000
--- a/src/library/hidden_defs.cpp
+++ /dev/null
@@ -1,87 +0,0 @@
-/*
-Copyright (c) 2013 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#include "util/name.h"
-#include "util/sstream.h"
-#include "util/name_map.h"
-#include "kernel/environment.h"
-#include "kernel/builtin.h"
-#include "library/hidden_defs.h"
-#include "library/kernel_bindings.h"
-
-namespace lean {
-struct hidden_defs_extension : public environment_extension {
-    typedef name_map<bool> hidden_defs;
-    hidden_defs m_hidden_defs;
-
-    hidden_defs_extension const * get_parent() const {
-        return environment_extension::get_parent<hidden_defs_extension>();
-    }
-
-    bool is_hidden(name const & n) const {
-        auto it = m_hidden_defs.find(n);
-        if (it != m_hidden_defs.end())
-            return it->second;
-        hidden_defs_extension const * parent = get_parent();
-        return parent && parent->is_hidden(n);
-    }
-
-    void set_hidden_flag(name const & d, bool f) {
-        m_hidden_defs[d] = f;
-    }
-};
-
-struct hidden_defs_extension_initializer {
-    unsigned m_extid;
-    hidden_defs_extension_initializer() {
-        m_extid = environment_cell::register_extension([](){ return std::unique_ptr<environment_extension>(new hidden_defs_extension()); });
-    }
-};
-
-static hidden_defs_extension_initializer g_hidden_defs_extension_initializer;
-
-static hidden_defs_extension const & to_ext(ro_environment const & env) {
-    return env->get_extension<hidden_defs_extension>(g_hidden_defs_extension_initializer.m_extid);
-}
-
-static hidden_defs_extension & to_ext(environment const & env) {
-    return env->get_extension<hidden_defs_extension>(g_hidden_defs_extension_initializer.m_extid);
-}
-
-bool is_hidden(ro_environment const & env, name const & d) {
-    return to_ext(env).is_hidden(d);
-}
-
-void set_hidden_flag(environment const & env, name const & d, bool flag) {
-    if (!env->get_object(d).is_definition())
-        throw exception(sstream() << "'" << d << "' is not a definition");
-    to_ext(env).set_hidden_flag(d, flag);
-}
-
-void hide_builtin(environment const & env) {
-    for (auto c : { mk_implies_fn(), mk_iff_fn(), mk_not_fn(), mk_or_fn(), mk_and_fn(),
-                mk_forall_fn() })
-        set_hidden_flag(env, const_name(c));
-}
-
-static int is_hidden(lua_State * L) {
-    ro_shared_environment env(L, 1);
-    lua_pushboolean(L, is_hidden(env, to_name_ext(L, 2)));
-    return 1;
-}
-
-static int set_hidden_flag(lua_State * L) {
-    int nargs = lua_gettop(L);
-    rw_shared_environment env(L, 1);
-    set_hidden_flag(env, to_name_ext(L, 2), nargs <= 2 ? true : lua_toboolean(L, 3));
-    return 0;
-}
-
-void open_hidden_defs(lua_State * L) {
-    SET_GLOBAL_FUN(is_hidden,       "is_hidden");
-    SET_GLOBAL_FUN(set_hidden_flag, "set_hidden_flag");
-}
-}
diff --git a/src/library/hidden_defs.h b/src/library/hidden_defs.h
deleted file mode 100644
index 588c69a7e..000000000
--- a/src/library/hidden_defs.h
+++ /dev/null
@@ -1,37 +0,0 @@
-/*
-Copyright (c) 2013 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#pragma once
-#include "util/lua.h"
-namespace lean {
-class environment;
-class ro_environment;
-class name;
-/**
-   \brief Return true iff the definition named \c d is hidden in
-   the given environment.
-
-   This information is just a hint used by tactics and solvers.  For
-   example, unfold_tactic uses it to decide whether a definition
-   should be unfolded or not.
-*/
-bool is_hidden(ro_environment const & env, name const & d);
-/**
-   \brief Mark the definition named \c d as hidden in the given environment.
-
-   \see is_hidden
-
-   \remark It throws an exception if \c d is not a definition in \c env.
-*/
-void set_hidden_flag(environment const & env, name const & d, bool flag = true);
-/**
-   \brief Hide definitions at builtin.cpp. We hide them here because
-   the hidden_defs module is not part of the kernel.
-*/
-void hide_builtin(environment const & env);
-
-void open_hidden_defs(lua_State * L);
-}
diff --git a/src/library/kernel_bindings.cpp b/src/library/kernel_bindings.cpp
index cc86d2341..1e5c49066 100644
--- a/src/library/kernel_bindings.cpp
+++ b/src/library/kernel_bindings.cpp
@@ -1121,6 +1121,19 @@ static int environment_tostring(lua_State * L) {
     return 1;
 }
 
+static int environment_set_opaque(lua_State * L) {
+    rw_shared_environment env(L, 1);
+    env->set_opaque(to_name_ext(L, 2), lua_toboolean(L, 3));
+    return 0;
+}
+
+static int environment_is_opaque(lua_State * L) {
+    ro_shared_environment env(L, 1);
+    auto obj = env->find_object(to_name_ext(L, 2));
+    lua_pushboolean(L, obj && obj->is_opaque());
+    return 1;
+}
+
 static const struct luaL_Reg environment_m[] = {
     {"__gc",           environment_gc}, // never throws
     {"__tostring",     safe_function<environment_tostring>},
@@ -1142,6 +1155,8 @@ static const struct luaL_Reg environment_m[] = {
     {"normalize",      safe_function<environment_normalize>},
     {"objects",        safe_function<environment_objects>},
     {"local_objects",  safe_function<environment_local_objects>},
+    {"set_opaque",     safe_function<environment_set_opaque>},
+    {"is_opaque",      safe_function<environment_is_opaque>},
     {0, 0}
 };
 
diff --git a/src/library/register_module.h b/src/library/register_module.h
index a668791b7..9ee5685ab 100644
--- a/src/library/register_module.h
+++ b/src/library/register_module.h
@@ -9,7 +9,6 @@ Author: Leonardo de Moura
 #include "library/kernel_bindings.h"
 #include "library/io_state.h"
 #include "library/type_inferer.h"
-#include "library/hidden_defs.h"
 #include "library/substitution.h"
 #include "library/fo_unify.h"
 #include "library/placeholder.h"
@@ -19,7 +18,6 @@ inline void open_core_module(lua_State * L) {
     open_kernel_module(L);
     open_io_state(L);
     open_type_inferer(L);
-    open_hidden_defs(L);
     open_substitution(L);
     open_fo_unify(L);
     open_placeholder(L);
diff --git a/src/library/tactic/tactic.cpp b/src/library/tactic/tactic.cpp
index d7720a4c1..0a866ee09 100644
--- a/src/library/tactic/tactic.cpp
+++ b/src/library/tactic/tactic.cpp
@@ -15,7 +15,6 @@ Author: Leonardo de Moura
 #include "kernel/replace_visitor.h"
 #include "kernel/instantiate.h"
 #include "kernel/update_expr.h"
-#include "library/hidden_defs.h"
 #include "library/kernel_bindings.h"
 #include "library/tactic/tactic.h"
 
@@ -397,7 +396,7 @@ protected:
 
     virtual expr visit_constant(expr const & c, context const &) {
         optional<object> obj = m_env->find_object(const_name(c));
-        if (obj && obj->is_definition() && !obj->is_opaque() && !is_hidden(m_env, const_name(c))) {
+        if (should_unfold(obj)) {
             m_unfolded = true;
             return obj->get_value();
         } else {
diff --git a/src/library/tactic/tactic.h b/src/library/tactic/tactic.h
index 1e44e154b..53b66a6a5 100644
--- a/src/library/tactic/tactic.h
+++ b/src/library/tactic/tactic.h
@@ -294,7 +294,7 @@ inline tactic focus(tactic const & t) { return focus(t, 1); }
 */
 tactic unfold_tactic(name const & n);
 /**
-   \brief Return a tactic that unfolds all (non-hidden and non-opaque) definitions.
+   \brief Return a tactic that unfolds all (non-opaque) definitions.
 */
 tactic unfold_tactic();
 /**
diff --git a/src/library/type_inferer.cpp b/src/library/type_inferer.cpp
index 8ea0523df..1cb361d2d 100644
--- a/src/library/type_inferer.cpp
+++ b/src/library/type_inferer.cpp
@@ -32,8 +32,8 @@ class type_inferer::imp {
     normalizer                m_normalizer;
     cache                     m_cache;
 
-    expr normalize(expr const & e, context const & ctx) {
-        return m_normalizer(e, ctx, m_menv.to_some_menv());
+    expr normalize(expr const & e, context const & ctx, bool unfold_opaque) {
+        return m_normalizer(e, ctx, m_menv.to_some_menv(), unfold_opaque);
     }
     expr lift_free_vars(expr const & e, unsigned s, unsigned d) {
         return ::lean::lift_free_vars(e, s, d, m_menv.to_some_menv());
@@ -52,7 +52,7 @@ class type_inferer::imp {
             return e;
         if (is_bool(e))
             return Type();
-        expr u = normalize(e, ctx);
+        expr u = normalize(e, ctx, false);
         if (is_type(u))
             return u;
         if (is_bool(u))
@@ -62,6 +62,11 @@ class type_inferer::imp {
             m_uc->push_back(mk_convertible_constraint(ctx, u, TypeU, jst));
             return u;
         }
+        u = normalize(e, ctx, true);
+        if (is_type(u))
+            return u;
+        if (is_bool(u))
+            return Type();
         throw type_expected_exception(m_env, ctx, s);
     }
 
@@ -72,7 +77,7 @@ class type_inferer::imp {
             if (is_pi(t)) {
                 t = abst_body(t);
             } else {
-                t = m_normalizer(t, ctx);
+                t = normalize(t, ctx, false);
                 if (is_pi(t)) {
                     t = abst_body(t);
                 } else if (has_metavar(t) && m_menv && m_uc) {
@@ -85,7 +90,12 @@ class type_inferer::imp {
                     m_uc->push_back(mk_eq_constraint(ctx, t, p, jst));
                     t        = abst_body(p);
                 } else {
-                    throw function_expected_exception(m_env, ctx, e);
+                    t = normalize(t, ctx, true);
+                    if (is_pi(t)) {
+                        t = abst_body(t);
+                    } else {
+                        throw function_expected_exception(m_env, ctx, e);
+                    }
                 }
             }
         }
@@ -249,7 +259,7 @@ public:
         if (is_bool(t))
             return true;
         else
-            return is_bool(normalize(t, ctx));
+            return is_bool(normalize(t, ctx, true));
     }
 };
 type_inferer::type_inferer(ro_environment const & env):m_ptr(new imp(env)) {}
diff --git a/src/tests/kernel/environment.cpp b/src/tests/kernel/environment.cpp
index 4025fa2c1..374ab09c6 100644
--- a/src/tests/kernel/environment.cpp
+++ b/src/tests/kernel/environment.cpp
@@ -121,7 +121,8 @@ static void tst4() {
     env->add_definition("b", Int, iAdd(Const("a"), iVal(1)));
     expr t2 = iSub(Const("b"), iVal(9));
     std::cout << t2 << " --> " << normalize(t2, env) << "\n";
-    lean_assert(normalize(t2, env) == iAdd(iAdd(Const("a"), iVal(1)), iVal(-9)));
+    lean_assert_eq(normalize(t2, env, context()),
+                   iSub(iAdd(Const("a"), iVal(1)), iVal(9)));
 }
 
 static void tst5() {
diff --git a/src/tests/library/arith.cpp b/src/tests/library/arith.cpp
index a4f6b4879..bbf71aa2b 100644
--- a/src/tests/library/arith.cpp
+++ b/src/tests/library/arith.cpp
@@ -95,15 +95,15 @@ static void tst4() {
     expr e = iSub(iVal(10), iVal(30));
     std::cout << e << "\n";
     std::cout << normalize(e, env) << "\n";
-    lean_assert(normalize(e, env) == iVal(-20));
+    lean_assert(normalize(e, env, context(), true) == iVal(-20));
     std::cout << infer_type(mk_int_sub_fn(), env) << "\n";
     lean_assert(infer_type(e, env) == Int);
     lean_assert(infer_type(mk_app(mk_int_sub_fn(), iVal(10)), env) == mk_arrow(Int, Int));
-    lean_assert(is_int_value(normalize(e, env)));
+    lean_assert(is_int_value(normalize(e, env, context(), true)));
     expr e2 = Fun("a", Int, iSub(Const("a"), iSub(iVal(10), iVal(30))));
     std::cout << e2 << " --> " << normalize(e2, env) << "\n";
     lean_assert(infer_type(e2, env) == (Int >> Int));
-    lean_assert(normalize(e2, env) == Fun("a", Int, iAdd(Const("a"), iVal(20))));
+    lean_assert_eq(normalize(e2, env, context(), true), Fun("a", Int, iAdd(Const("a"), iVal(20))));
 }
 
 static void tst5() {
diff --git a/tests/lean/interactive/elab6.lean b/tests/lean/interactive/elab6.lean
index 9cf23fdbd..339fc7e5f 100644
--- a/tests/lean/interactive/elab6.lean
+++ b/tests/lean/interactive/elab6.lean
@@ -1,9 +1,9 @@
 (**
--- The elaborator does not expand definitions marked as 'hidden'.
+-- The elaborator does not expand definitions marked as 'opaque'.
 -- To be able to prove the following theorem, we have to unmark the
 -- 'forall'
 local env = get_environment()
-set_hidden_flag(env, "forall", false)
+env:set_opaque("forall", false)
 **)
 Theorem ForallIntro2 (A : (Type U)) (P : A -> Bool) (H : Pi x, P x) : forall x, P x :=
         Abst (fun x, EqTIntro (H x))
diff --git a/tests/lua/hidden1.lua b/tests/lua/hidden1.lua
index 2927aaa85..4222bac49 100644
--- a/tests/lua/hidden1.lua
+++ b/tests/lua/hidden1.lua
@@ -1,14 +1,13 @@
 local env = environment()
-assert(is_hidden(env, "and"))
-assert(is_hidden(env, "or"))
-assert(is_hidden(env, {"Int", "lt"}))
+assert(env:is_opaque("and"))
+assert(env:is_opaque("or"))
+assert(env:is_opaque({"Int", "lt"}))
 parse_lean_cmds([[
   Definition a : Bool := true
 ]], env)
-assert(not is_hidden(env, "a"))
-set_hidden_flag(env, "a")
-assert(is_hidden(env, "a"))
-set_hidden_flag(env, "a", false)
-assert(not is_hidden(env, "a"))
-assert(not is_hidden(env, "b"))
-assert(not pcall(function () set_hidden_flag(env, "b") end))
+assert(not env:is_opaque("a"))
+env:set_opaque("a", true)
+assert(env:is_opaque("a"))
+env:set_opaque("a", false)
+assert(not env:is_opaque("a"))
+assert(not env:is_opaque("b"))