diff --git a/src/kernel/arith/arith.cpp b/src/kernel/arith/arith.cpp
index b8d258943..211bd47a7 100644
--- a/src/kernel/arith/arith.cpp
+++ b/src/kernel/arith/arith.cpp
@@ -25,8 +25,8 @@ public:
 };
 
 char const * int_type_value::g_kind = "int";
-
-MK_BUILTIN(int_type, int_type_value);
+expr const Int = mk_value(*(new int_type_value()));
+expr mk_int_type() { return Int; }
 
 class int_value_value : public value {
     mpz m_val;
diff --git a/src/kernel/arith/arith.h b/src/kernel/arith/arith.h
index a30159c84..1d7895bf3 100644
--- a/src/kernel/arith/arith.h
+++ b/src/kernel/arith/arith.h
@@ -12,7 +12,7 @@ Author: Leonardo de Moura
 
 namespace lean {
 expr mk_int_type();
-#define Int mk_int_type()
+extern expr const Int;
 
 expr mk_int_value(mpz const & v);
 inline expr mk_int_value(int v) { return mk_int_value(mpz(v)); }
diff --git a/src/kernel/builtin.cpp b/src/kernel/builtin.cpp
index e6b4acb4b..355d738d8 100644
--- a/src/kernel/builtin.cpp
+++ b/src/kernel/builtin.cpp
@@ -50,16 +50,8 @@ expr mk_bin_lop(expr const & op, expr const & unit, std::initializer_list<expr>
 // Bultin universe variables m and u
 static level m_lvl(name("m"));
 static level u_lvl(name("u"));
-
-expr mk_type_m() {
-    static thread_local expr r = Type(m_lvl);
-    return r;
-}
-
-expr mk_type_u() {
-    static thread_local expr r = Type(u_lvl);
-    return r;
-}
+expr const TypeM = Type(m_lvl);
+expr const TypeU = Type(u_lvl);
 // =======================================
 
 // =======================================
@@ -79,7 +71,8 @@ public:
     virtual unsigned hash() const { return 17; }
 };
 char const * bool_type_value::g_kind = g_Bool_str;
-MK_BUILTIN(bool_type, bool_type_value);
+expr const Bool = mk_value(*(new bool_type_value()));
+expr mk_bool_type() { return Bool; }
 // =======================================
 
 // =======================================
@@ -116,10 +109,10 @@ public:
     bool get_val() const { return m_val; }
 };
 char const * bool_value_value::g_kind = "BoolValue";
+expr const True  = mk_value(*(new bool_value_value(true)));
+expr const False = mk_value(*(new bool_value_value(false)));
 expr mk_bool_value(bool v) {
-    static thread_local expr true_val  = mk_value(*(new bool_value_value(true)));
-    static thread_local expr false_val = mk_value(*(new bool_value_value(false)));
-    return v ? true_val : false_val;
+    return v ? True : False;
 }
 bool is_bool_value(expr const & e) {
     return is_value(e) && to_value(e).kind() == bool_value_value::g_kind;
diff --git a/src/kernel/builtin.h b/src/kernel/builtin.h
index 3a3f37644..3c7104df9 100644
--- a/src/kernel/builtin.h
+++ b/src/kernel/builtin.h
@@ -23,21 +23,19 @@ expr mk_bin_lop(expr const & op, expr const & unit, unsigned num_args, expr cons
 expr mk_bin_lop(expr const & op, expr const & unit, std::initializer_list<expr> const & l);
 
 /** \brief Return (Type m)  m >= bottom + Offset */
-expr mk_type_m();
-#define TypeM mk_type_m()
+extern expr const TypeM;
 
 /** \brief Return (Type u)  u >= m + Offset */
-expr mk_type_u();
-#define TypeU mk_type_u()
+extern expr const TypeU;
 
 /** \brief Return the Lean Boolean type. */
 expr mk_bool_type();
-#define Bool mk_bool_type()
+extern expr const Bool;
 
 /** \brief Create a Lean Boolean value (true/false) */
 expr mk_bool_value(bool v);
-#define True  mk_bool_value(true)
-#define False mk_bool_value(false)
+extern expr const True;
+extern expr const False;
 /** \brief Return true iff \c e is a Lean Boolean value. */
 bool is_bool_value(expr const & e);
 /**