diff --git a/src/kernel/deep_copy.cpp b/src/kernel/deep_copy.cpp
index 32459dcd3..dcc116452 100644
--- a/src/kernel/deep_copy.cpp
+++ b/src/kernel/deep_copy.cpp
@@ -23,7 +23,7 @@ class deep_copy_fn {
         }
         expr r;
         switch (a.kind()) {
-        case expr_kind::Var: case expr_kind::Constant: case expr_kind::Type: case expr_kind::Numeral:
+        case expr_kind::Var: case expr_kind::Constant: case expr_kind::Type: case expr_kind::Value:
             r = copy(a); break; // shallow copy is equivalent to deep copy for these ones.
         case expr_kind::App: {
             buffer<expr> new_args;
diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp
index d3c35d707..ee7e78571 100644
--- a/src/kernel/expr.cpp
+++ b/src/kernel/expr.cpp
@@ -29,10 +29,9 @@ expr_var::expr_var(unsigned idx):
     expr_cell(expr_kind::Var, idx),
     m_vidx(idx) {}
 
-expr_const::expr_const(name const & n, unsigned pos):
+expr_const::expr_const(name const & n):
     expr_cell(expr_kind::Constant, n.hash()),
-    m_name(n),
-    m_pos(pos) {}
+    m_name(n) {}
 
 expr_app::expr_app(unsigned num_args):
     expr_cell(expr_kind::App, 0),
@@ -90,9 +89,15 @@ expr_type::expr_type(level const & l):
 }
 expr_type::~expr_type() {
 }
-expr_numeral::expr_numeral(mpz const & n):
-    expr_cell(expr_kind::Numeral, n.hash()),
-    m_numeral(n) {}
+
+expr_value::expr_value(value & v):
+    expr_cell(expr_kind::Value, v.hash()),
+    m_val(v) {
+    m_val.inc_ref();
+}
+expr_value::~expr_value() {
+    m_val.dec_ref();
+}
 
 void expr_cell::dealloc() {
     switch (kind()) {
@@ -102,7 +107,7 @@ void expr_cell::dealloc() {
     case expr_kind::Lambda:     delete static_cast<expr_lambda*>(this); break;
     case expr_kind::Pi:         delete static_cast<expr_pi*>(this); break;
     case expr_kind::Type:       delete static_cast<expr_type*>(this); break;
-    case expr_kind::Numeral:    delete static_cast<expr_numeral*>(this); break;
+    case expr_kind::Value:      delete static_cast<expr_value*>(this); break;
     }
 }
 
@@ -136,7 +141,7 @@ class eq_fn {
             // Remark: we ignore get_abs_name because we want alpha-equivalence
             return apply(abst_domain(a), abst_domain(b)) && apply(abst_body(a), abst_body(b));
         case expr_kind::Type:     return ty_level(a) == ty_level(b);
-        case expr_kind::Numeral:  return num_value(a) == num_value(b);
+        case expr_kind::Value:    return to_value(a) == to_value(b);
         }
         lean_unreachable();
         return false;
@@ -185,7 +190,7 @@ std::ostream & operator<<(std::ostream & out, expr const & a) {
             out << "(Type " << ty_level(a) << ")";
         break;
     }
-    case expr_kind::Numeral: out << num_value(a); break;
+    case expr_kind::Value: to_value(a).display(out); break;
     }
     return out;
 }
@@ -193,9 +198,9 @@ std::ostream & operator<<(std::ostream & out, expr const & a) {
 expr copy(expr const & a) {
     switch (a.kind()) {
     case expr_kind::Var:      return var(var_idx(a));
-    case expr_kind::Constant: return constant(const_name(a), const_pos(a));
+    case expr_kind::Constant: return constant(const_name(a));
     case expr_kind::Type:     return type(ty_level(a));
-    case expr_kind::Numeral:  return numeral(num_value(a));
+    case expr_kind::Value:    return to_expr(static_cast<expr_value*>(a.raw())->m_val);
     case expr_kind::App:      return app(num_args(a), begin_args(a));
     case expr_kind::Lambda:   return lambda(abst_name(a), abst_domain(a), abst_body(a));
     case expr_kind::Pi:       return pi(abst_name(a), abst_domain(a), abst_body(a));
@@ -212,6 +217,8 @@ lean::format pp_aux(lean::expr const & a) {
         return format{format("#"), format(static_cast<int>(var_idx(a)))};
     case expr_kind::Constant:
         return format(const_name(a));
+    case expr_kind::Value:
+        return to_value(a).pp();
     case expr_kind::App:
     {
         format r;
@@ -247,8 +254,6 @@ lean::format pp_aux(lean::expr const & a) {
         return paren(format{format("Type "),
                             format(ss.str())});
     }
-    case expr_kind::Numeral:
-        return format(num_value(a));
     }
     lean_unreachable();
     return format();
diff --git a/src/kernel/expr.h b/src/kernel/expr.h
index 2fe847d76..5d450b33b 100644
--- a/src/kernel/expr.h
+++ b/src/kernel/expr.h
@@ -9,21 +9,22 @@ Author: Leonardo de Moura
 #include <limits>
 #include "rc.h"
 #include "name.h"
-#include "mpz.h"
 #include "level.h"
 #include "hash.h"
 #include "buffer.h"
+#include "format.h"
 
 namespace lean {
+class value;
 /* =======================================
    Expressions
-   expr ::=   Var      idx
-          |   Constant name
-          |   App      [expr]
-          |   Lambda   name expr expr
-          |   Pi       name expr expr
-          |   Type     universe
-          |   Numeral  value
+   expr ::=   Var           idx
+          |   Constant      name
+          |   Value         value
+          |   App           [expr]
+          |   Lambda        name expr expr
+          |   Pi            name expr expr
+          |   Type          universe
 
 TODO: add meta-variables, let, constructor references and match.
 
@@ -33,7 +34,7 @@ The main API is divided in the following sections
 - Accessors
 - Miscellaneous
 ======================================= */
-enum class expr_kind { Var, Constant, App, Lambda, Pi, Type, Numeral };
+enum class expr_kind { Var, Constant, Value, App, Lambda, Pi, Type };
 
 /**
     \brief Base class used to represent expressions.
@@ -92,14 +93,13 @@ public:
 
     friend expr var(unsigned idx);
     friend expr constant(name const & n);
-    friend expr constant(name const & n, unsigned pos);
+    friend expr to_expr(value & v);
     friend expr app(unsigned num_args, expr const * args);
     friend expr app(std::initializer_list<expr> const & l);
     friend expr lambda(name const & n, expr const & t, expr const & e);
     friend expr pi(name const & n, expr const & t, expr const & e);
     friend expr prop();
     friend expr type(level const & l);
-    friend expr numeral(mpz const & n);
 
     friend bool eqp(expr const & a, expr const & b) { return a.m_ptr == b.m_ptr; }
 
@@ -122,11 +122,9 @@ public:
 /** \brief Constants. */
 class expr_const : public expr_cell {
     name     m_name;
-    unsigned m_pos;  // position in the environment.
 public:
-    expr_const(name const & n, unsigned pos = std::numeric_limits<unsigned>::max());
+    expr_const(name const & n);
     name const & get_name() const { return m_name; }
-    unsigned     get_pos() const { return m_pos; }
 };
 /** \brief Function Applications */
 class expr_app : public expr_cell {
@@ -170,33 +168,55 @@ public:
     ~expr_type();
     level const & get_level() const { return m_level; }
 };
-/** \brief Numerals (efficient encoding using GMP numbers) */
-class expr_numeral : public expr_cell {
-    mpz   m_numeral;
+/**
+   \brief Base class for semantic attachment cells.
+*/
+class value {
+    void dealloc() { delete this; }
+    MK_LEAN_RC();
 public:
-    expr_numeral(mpz const & n);
-    mpz const & get_num() const { return m_numeral; }
+    value():m_rc(0) {}
+    virtual ~value() {}
+    virtual char const * kind() const = 0;
+    virtual expr get_type() const = 0;
+    virtual expr normalize(unsigned num_args, expr const * args) const = 0;
+    virtual bool operator==(value const & other) const = 0;
+    virtual void display(std::ostream & out) const = 0;
+    virtual format pp() const = 0;
+    virtual unsigned hash() const = 0;
+};
+
+/** \brief Semantic attachments */
+class expr_value : public expr_cell {
+    value & m_val;
+    friend expr copy(expr const & a);
+public:
+    expr_value(value & v);
+    ~expr_value();
+
+    value const & get_value() const { return m_val; }
 };
 // =======================================
 
+
 // =======================================
 // Testers
 inline bool is_var(expr_cell * e)         { return e->kind() == expr_kind::Var; }
 inline bool is_constant(expr_cell * e)    { return e->kind() == expr_kind::Constant; }
+inline bool is_value(expr_cell * e)       { return e->kind() == expr_kind::Value; }
 inline bool is_app(expr_cell * e)         { return e->kind() == expr_kind::App; }
 inline bool is_lambda(expr_cell * e)      { return e->kind() == expr_kind::Lambda; }
 inline bool is_pi(expr_cell * e)          { return e->kind() == expr_kind::Pi; }
 inline bool is_type(expr_cell * e)        { return e->kind() == expr_kind::Type; }
-inline bool is_numeral(expr_cell * e)     { return e->kind() == expr_kind::Numeral; }
 inline bool is_abstraction(expr_cell * e) { return is_lambda(e) || is_pi(e); }
 
 inline bool is_var(expr const & e)         { return e.kind() == expr_kind::Var; }
 inline bool is_constant(expr const & e)    { return e.kind() == expr_kind::Constant; }
+inline bool is_value(expr const & e)       { return e.kind() == expr_kind::Value; }
 inline bool is_app(expr const & e)         { return e.kind() == expr_kind::App; }
 inline bool is_lambda(expr const & e)      { return e.kind() == expr_kind::Lambda; }
 inline bool is_pi(expr const & e)          { return e.kind() == expr_kind::Pi; }
 inline bool is_type(expr const & e)        { return e.kind() == expr_kind::Type; }
-inline bool is_numeral(expr const & e)     { return e.kind() == expr_kind::Numeral; }
 inline bool is_abstraction(expr const & e) { return is_lambda(e) || is_pi(e); }
 // =======================================
 
@@ -205,7 +225,7 @@ inline bool is_abstraction(expr const & e) { return is_lambda(e) || is_pi(e); }
 inline expr var(unsigned idx) { return expr(new expr_var(idx)); }
 inline expr constant(name const & n) { return expr(new expr_const(n)); }
 inline expr constant(char const * n) { return constant(name(n)); }
-inline expr constant(name const & n, unsigned pos) { return expr(new expr_const(n, pos)); }
+inline expr to_expr(value & v) { return expr(new expr_value(v)); }
        expr app(unsigned num_args, expr const * args);
 inline expr app(expr const & e1, expr const & e2) { expr args[2] = {e1, e2}; return app(2, args); }
 inline expr app(expr const & e1, expr const & e2, expr const & e3) { expr args[3] = {e1, e2, e3}; return app(3, args); }
@@ -217,8 +237,6 @@ inline expr pi(name const & n, expr const & t, expr const & e) { return expr(new
 inline expr pi(char const * n, expr const & t, expr const & e) { return pi(name(n), t, e); }
 inline expr arrow(expr const & t, expr const & e) { return pi(name("_"), t, e); }
 inline expr type(level const & l) { return expr(new expr_type(l)); }
-inline expr numeral(mpz const & n) { return expr(new expr_numeral(n)); }
-inline expr numeral(int n) { return numeral(mpz(n)); }
 
 inline expr expr::operator()(expr const & a1) const { return app(*this, a1); }
 inline expr expr::operator()(expr const & a1, expr const & a2) const { return app(*this, a1, a2); }
@@ -235,7 +253,6 @@ inline expr_abstraction * to_abstraction(expr_cell * e) { lean_assert(is_abstrac
 inline expr_lambda *      to_lambda(expr_cell * e)      { lean_assert(is_lambda(e));      return static_cast<expr_lambda*>(e); }
 inline expr_pi *          to_pi(expr_cell * e)          { lean_assert(is_pi(e));          return static_cast<expr_pi*>(e); }
 inline expr_type *        to_type(expr_cell * e)        { lean_assert(is_type(e));        return static_cast<expr_type*>(e); }
-inline expr_numeral *     to_numeral(expr_cell * e)     { lean_assert(is_numeral(e));     return static_cast<expr_numeral*>(e); }
 
 inline expr_var *         to_var(expr const & e)         { return to_var(e.raw()); }
 inline expr_const *       to_constant(expr const & e)    { return to_constant(e.raw()); }
@@ -244,7 +261,6 @@ inline expr_abstraction * to_abstraction(expr const & e) { return to_abstraction
 inline expr_lambda *      to_lambda(expr const & e)      { return to_lambda(e.raw()); }
 inline expr_pi *          to_pi(expr const & e)          { return to_pi(e.raw()); }
 inline expr_type *        to_type(expr const & e)        { return to_type(e.raw()); }
-inline expr_numeral *     to_numeral(expr const & e)     { return to_numeral(e.raw()); }
 // =======================================
 
 // =======================================
@@ -254,21 +270,20 @@ inline bool          is_shared(expr_cell * e)            { return get_rc(e) > 1;
 inline unsigned      var_idx(expr_cell * e)              { return to_var(e)->get_vidx(); }
 inline bool          is_var(expr_cell * e, unsigned i)   { return is_var(e) && var_idx(e) == i; }
 inline name const &  const_name(expr_cell * e)           { return to_constant(e)->get_name(); }
-inline unsigned      const_pos(expr_cell * e)            { return to_constant(e)->get_pos(); }
+inline value const & to_value(expr_cell * e)             { lean_assert(is_value(e)); return static_cast<expr_value*>(e)->get_value(); }
 inline unsigned      num_args(expr_cell * e)             { return to_app(e)->get_num_args(); }
 inline expr const &  arg(expr_cell * e, unsigned idx)    { return to_app(e)->get_arg(idx); }
 inline name const &  abst_name(expr_cell * e)            { return to_abstraction(e)->get_name(); }
 inline expr const &  abst_domain(expr_cell * e)          { return to_abstraction(e)->get_domain(); }
 inline expr const &  abst_body(expr_cell * e)            { return to_abstraction(e)->get_body(); }
 inline level const & ty_level(expr_cell * e)             { return to_type(e)->get_level(); }
-inline mpz const &   num_value(expr_cell * e)            { return to_numeral(e)->get_num(); }
 
 inline unsigned      get_rc(expr const &  e)              { return e.raw()->get_rc(); }
 inline bool          is_shared(expr const & e)            { return get_rc(e) > 1; }
 inline unsigned      var_idx(expr const & e)              { return to_var(e)->get_vidx(); }
 inline bool          is_var(expr const & e, unsigned i)   { return is_var(e) && var_idx(e) == i; }
 inline name const &  const_name(expr const & e)           { return to_constant(e)->get_name(); }
-inline unsigned      const_pos(expr const & e)            { return to_constant(e)->get_pos(); }
+inline value const & to_value(expr const & e)             { return to_value(e.raw()); }
 inline unsigned      num_args(expr const & e)             { return to_app(e)->get_num_args(); }
 inline expr const &  arg(expr const & e, unsigned idx)    { return to_app(e)->get_arg(idx); }
 inline expr const *  begin_args(expr const & e)           { return to_app(e)->begin_args(); }
@@ -277,7 +292,6 @@ inline name const &  abst_name(expr const & e)            { return to_abstractio
 inline expr const &  abst_domain(expr const & e)          { return to_abstraction(e)->get_domain(); }
 inline expr const &  abst_body(expr const & e)            { return to_abstraction(e)->get_body(); }
 inline level const & ty_level(expr const & e)             { return to_type(e)->get_level(); }
-inline mpz const &   num_value(expr const & e)            { return to_numeral(e)->get_num(); }
 // =======================================
 
 // =======================================
diff --git a/src/kernel/free_vars.cpp b/src/kernel/free_vars.cpp
index b0d11b988..068be0b97 100644
--- a/src/kernel/free_vars.cpp
+++ b/src/kernel/free_vars.cpp
@@ -23,7 +23,7 @@ protected:
     bool apply(expr const & e, unsigned offset) {
         // handle easy cases
         switch (e.kind()) {
-        case expr_kind::Constant: case expr_kind::Type: case expr_kind::Numeral:
+        case expr_kind::Constant: case expr_kind::Type: case expr_kind::Value:
             return false;
         case expr_kind::Var:
             return process_var(e, offset);
@@ -44,7 +44,7 @@ protected:
         bool result = false;
 
         switch (e.kind()) {
-        case expr_kind::Constant: case expr_kind::Type: case expr_kind::Numeral: case expr_kind::Var:
+        case expr_kind::Constant: case expr_kind::Type: case expr_kind::Value: case expr_kind::Var:
             // easy cases were already handled
             lean_unreachable(); return false;
         case expr_kind::App:
diff --git a/src/kernel/max_sharing.cpp b/src/kernel/max_sharing.cpp
index edd97fbd9..033118803 100644
--- a/src/kernel/max_sharing.cpp
+++ b/src/kernel/max_sharing.cpp
@@ -32,7 +32,7 @@ struct max_sharing_fn::imp {
             return a;
         }
         switch (a.kind()) {
-        case expr_kind::Var: case expr_kind::Constant: case expr_kind::Type: case expr_kind::Numeral:
+        case expr_kind::Var: case expr_kind::Constant: case expr_kind::Type: case expr_kind::Value:
             cache(a);
             return a;
         case expr_kind::App: {
diff --git a/src/kernel/normalize.cpp b/src/kernel/normalize.cpp
index 175ff4be0..35de6e1a5 100644
--- a/src/kernel/normalize.cpp
+++ b/src/kernel/normalize.cpp
@@ -18,18 +18,18 @@ Author: Leonardo de Moura
 namespace lean {
 
 class svalue;
-typedef list<svalue> stack; //!< Normalization stack
+typedef list<svalue> value_stack; //!< Normalization stack
 enum class svalue_kind { Expr, Closure, BoundedVar };
 /** \brief Stack value: simple expressions, closures and bounded variables. */
 class svalue {
     svalue_kind m_kind;
     unsigned    m_bvar;
     expr        m_expr;
-    stack       m_ctx;
+    value_stack m_ctx;
 public:
-    explicit svalue(expr const & e):        m_kind(svalue_kind::Expr), m_expr(e) {}
-    explicit svalue(unsigned k):            m_kind(svalue_kind::BoundedVar), m_bvar(k) {}
-    svalue(expr const & e, stack const & c):m_kind(svalue_kind::Closure), m_expr(e), m_ctx(c) { lean_assert(is_lambda(e)); }
+    explicit svalue(expr const & e):              m_kind(svalue_kind::Expr), m_expr(e) {}
+    explicit svalue(unsigned k):                  m_kind(svalue_kind::BoundedVar), m_bvar(k) {}
+    svalue(expr const & e, value_stack const & c):m_kind(svalue_kind::Closure), m_expr(e), m_ctx(c) { lean_assert(is_lambda(e)); }
 
     svalue_kind kind() const { return m_kind; }
 
@@ -38,25 +38,25 @@ public:
     bool is_bounded_var() const { return kind() == svalue_kind::BoundedVar; }
 
     expr  const & get_expr() const { lean_assert(is_expr() || is_closure()); return m_expr; }
-    stack const & get_ctx()  const { lean_assert(is_closure());              return m_ctx; }
+    value_stack const & get_ctx()  const { lean_assert(is_closure());              return m_ctx; }
     unsigned get_var_idx()   const { lean_assert(is_bounded_var());          return m_bvar; }
 };
 
-svalue_kind   kind(svalue const & v)     { return v.kind(); }
-expr const &  to_expr(svalue const & v)  { return v.get_expr(); }
-stack const & stack_of(svalue const & v) { return v.get_ctx(); }
-unsigned      to_bvar(svalue const & v)  { return v.get_var_idx(); }
+svalue_kind         kind(svalue const & v)     { return v.kind(); }
+expr const &        to_expr(svalue const & v)  { return v.get_expr(); }
+value_stack const & stack_of(svalue const & v) { return v.get_ctx(); }
+unsigned            to_bvar(svalue const & v)  { return v.get_var_idx(); }
 
-stack extend(stack const & s, svalue const & v) { return cons(v, s); }
+value_stack extend(value_stack const & s, svalue const & v) { return cons(v, s); }
 
 /** \brief Expression normalizer. */
 class normalize_fn {
     environment const & m_env;
     context     const & m_ctx;
 
-    svalue lookup(stack const & s, unsigned i, unsigned k) {
+    svalue lookup(value_stack const & s, unsigned i, unsigned k) {
         unsigned j = i;
-        stack const * it1 = &s;
+        value_stack const * it1 = &s;
         while (*it1) {
             if (j == 0)
                 return head(*it1);
@@ -75,7 +75,7 @@ class normalize_fn {
     }
 
     /** \brief Convert the closure \c a into an expression using the given stack in a context that contains \c k binders. */
-    expr reify_closure(expr const & a, stack const & s, unsigned k) {
+    expr reify_closure(expr const & a, value_stack const & s, unsigned k) {
         lean_assert(is_lambda(a));
         expr new_t = reify(normalize(abst_domain(a), s, k), k);
         expr new_b = reify(normalize(abst_body(a), extend(s, svalue(k)), k+1), k+1);
@@ -126,12 +126,12 @@ class normalize_fn {
     }
 
     /** \brief Normalize the expression \c a in a context composed of stack \c s and \c k binders. */
-    svalue normalize(expr const & a, stack const & s, unsigned k) {
+    svalue normalize(expr const & a, value_stack const & s, unsigned k) {
         lean_trace("normalize", tout << "Normalize, k: " << k << "\n" << a << "\n";);
         switch (a.kind()) {
         case expr_kind::Var:
             return lookup(s, var_idx(a), k);
-        case expr_kind::Constant: case expr_kind::Type: case expr_kind::Numeral:
+        case expr_kind::Constant: case expr_kind::Type: case expr_kind::Value:
             return svalue(a);
         case expr_kind::App: {
             svalue f    = normalize(arg(a, 0), s, k);
@@ -142,7 +142,7 @@ class normalize_fn {
                     // beta reduction
                     expr const & fv = to_expr(f);
                     lean_trace("normalize", tout << "beta reduction...\n" << fv << "\n";);
-                    stack new_s = extend(stack_of(f), normalize(arg(a, i), s, k));
+                    value_stack new_s = extend(stack_of(f), normalize(arg(a, i), s, k));
                     f = normalize(abst_body(fv), new_s, k);
                     if (i == n - 1)
                         return f;
@@ -177,7 +177,7 @@ public:
 
     expr operator()(expr const & e) {
         unsigned k = length(m_ctx);
-        return reify(normalize(e, stack(), k), k);
+        return reify(normalize(e, value_stack(), k), k);
     }
 };
 
diff --git a/src/kernel/replace.h b/src/kernel/replace.h
index 298a1da09..01d90e94d 100644
--- a/src/kernel/replace.h
+++ b/src/kernel/replace.h
@@ -39,7 +39,7 @@ class replace_fn {
         expr r = m_f(e, offset);
         if (eqp(e, r)) {
             switch (e.kind()) {
-            case expr_kind::Type: case expr_kind::Numeral: case expr_kind::Constant: case expr_kind::Var:
+            case expr_kind::Type: case expr_kind::Value: case expr_kind::Constant: case expr_kind::Var:
                 break;
             case expr_kind::App:
                 r = update_app(e, [=](expr const & c) { return apply(c, offset); });
diff --git a/src/kernel/type_check.cpp b/src/kernel/type_check.cpp
index a8487bf74..e874ce0b4 100644
--- a/src/kernel/type_check.cpp
+++ b/src/kernel/type_check.cpp
@@ -110,9 +110,8 @@ class infer_type_fn {
             level l2 = infer_universe(abst_body(e), extend(ctx, abst_name(e), abst_domain(e)));
             return type(max(l1, l2));
         }
-        case expr_kind::Numeral:
-            // TODO
-            return e;
+        case expr_kind::Value:
+            return to_value(e).get_type();
         }
         lean_unreachable();
         return e;
diff --git a/src/tests/kernel/expr.cpp b/src/tests/kernel/expr.cpp
index ef1def0e0..bed285ec3 100644
--- a/src/tests/kernel/expr.cpp
+++ b/src/tests/kernel/expr.cpp
@@ -18,7 +18,7 @@ using namespace lean;
 
 void tst1() {
     expr a;
-    a = numeral(mpz(10));
+    a = constant("a");
     expr f;
     f = var(0);
     expr fa = f(a);
@@ -40,7 +40,7 @@ void tst1() {
 void tst1_pp() {
     std::cerr << "=============== PP =====================\n";
     expr a;
-    a = numeral(mpz(10));
+    a = constant("a");
     expr f;
     f = var(0);
     expr fa = f(a);
@@ -66,7 +66,7 @@ expr mk_dag(unsigned depth, bool _closed = false) {
 
 unsigned depth1(expr const & e) {
     switch (e.kind()) {
-    case expr_kind::Var: case expr_kind::Constant: case expr_kind::Type: case expr_kind::Numeral:
+    case expr_kind::Var: case expr_kind::Constant: case expr_kind::Type: case expr_kind::Value:
         return 1;
     case expr_kind::App: {
         unsigned m = 0;
@@ -83,7 +83,7 @@ unsigned depth1(expr const & e) {
 // This is the fastest depth implementation in this file.
 unsigned depth2(expr const & e) {
     switch (e.kind()) {
-    case expr_kind::Var: case expr_kind::Constant: case expr_kind::Type: case expr_kind::Numeral:
+    case expr_kind::Var: case expr_kind::Constant: case expr_kind::Type: case expr_kind::Value:
         return 1;
     case expr_kind::App:
         return
@@ -107,7 +107,7 @@ unsigned depth3(expr const & e) {
         unsigned c     = p.second + 1;
         todo.pop_back();
         switch (e.kind()) {
-        case expr_kind::Var: case expr_kind::Constant: case expr_kind::Type: case expr_kind::Numeral:
+        case expr_kind::Var: case expr_kind::Constant: case expr_kind::Type: case expr_kind::Value:
             m = std::max(c, m);
             break;
         case expr_kind::App: {
@@ -168,7 +168,7 @@ unsigned count_core(expr const & a, expr_set & s) {
         return 0;
     s.insert(a);
     switch (a.kind()) {
-    case expr_kind::Var: case expr_kind::Constant: case expr_kind::Type: case expr_kind::Numeral:
+    case expr_kind::Var: case expr_kind::Constant: case expr_kind::Type: case expr_kind::Value:
         return 1;
     case expr_kind::App:
         return std::accumulate(begin_args(a), end_args(a), 1,
@@ -232,7 +232,7 @@ void tst8() {
     expr f = constant("f");
     expr x = var(0);
     expr a = constant("a");
-    expr n = numeral(mpz(10));
+    expr n = constant("n");
     expr p = type(level());
     expr y = var(1);
     lean_assert(closed(a));
@@ -316,7 +316,7 @@ void tst12() {
     expr a = constant("a");
     expr x = var(0);
     expr t = type(level());
-    expr F = pi("y", t, lambda("x", t, f(f(f(x,a),numeral(10)),x)));
+    expr F = pi("y", t, lambda("x", t, f(f(f(x,a),constant("10")),x)));
     expr G = deep_copy(F);
     lean_assert(F == G);
     lean_assert(!eqp(F, G));
diff --git a/src/tests/kernel/normalize.cpp b/src/tests/kernel/normalize.cpp
index 07f4c137d..a5e3645dc 100644
--- a/src/tests/kernel/normalize.cpp
+++ b/src/tests/kernel/normalize.cpp
@@ -57,7 +57,7 @@ unsigned count_core(expr const & a, expr_set & s) {
         return 0;
     s.insert(a);
     switch (a.kind()) {
-    case expr_kind::Var: case expr_kind::Constant: case expr_kind::Type: case expr_kind::Numeral:
+    case expr_kind::Var: case expr_kind::Constant: case expr_kind::Type: case expr_kind::Value:
         return 1;
     case expr_kind::App:
         return std::accumulate(begin_args(a), end_args(a), 1,