diff --git a/src/library/vm.cpp b/src/library/vm.cpp
index b4901c4ac4..dff0aa277a 100644
--- a/src/library/vm.cpp
+++ b/src/library/vm.cpp
@@ -354,11 +354,11 @@ vm_instr & vm_instr::operator=(vm_instr && s) {
 }
 
 
-vm_decl_cell::vm_decl_cell(name const & n, unsigned arity, vm_function fn):
-    m_rc(0), m_builtin(true), m_name(n), m_arity(arity), m_fn(fn) {}
+vm_decl_cell::vm_decl_cell(name const & n, unsigned idx, unsigned arity, vm_function fn):
+    m_rc(0), m_builtin(true), m_name(n), m_idx(idx), m_arity(arity), m_fn(fn) {}
 
-vm_decl_cell::vm_decl_cell(name const & n, expr const & e, unsigned code_sz, vm_instr const * code):
-    m_rc(0), m_builtin(false), m_name(n), m_expr(e), m_arity(0),
+vm_decl_cell::vm_decl_cell(name const & n, unsigned idx, expr const & e, unsigned code_sz, vm_instr const * code):
+    m_rc(0), m_builtin(false), m_name(n), m_idx(idx), m_expr(e), m_arity(0),
     m_code_size(code_sz) {
     expr it = e;
     while (is_lambda(it)) {
@@ -398,8 +398,7 @@ struct vm_decls : public environment_extension {
 
     void add(vm_decl const & d) {
         lean_assert(!m_name2idx.contains(d.get_name()));
-        unsigned idx = m_decls.size();
-        m_name2idx.insert(d.get_name(), idx);
+        m_name2idx.insert(d.get_name(), d.get_idx());
         m_decls.push_back(d);
     }
 
@@ -407,7 +406,7 @@ struct vm_decls : public environment_extension {
         lean_assert(!m_name2idx.contains(n));
         unsigned idx = m_decls.size();
         m_name2idx.insert(n, idx);
-        m_decls.push_back(vm_decl(n, e, 0, nullptr));
+        m_decls.push_back(vm_decl(n, idx, e, 0, nullptr));
         return idx;
     }
 
@@ -415,14 +414,14 @@ struct vm_decls : public environment_extension {
         lean_assert(m_name2idx.contains(n));
         unsigned idx = *m_name2idx.find(n);
         vm_decl d    = m_decls[idx];
-        m_decls.set(idx, vm_decl(n, d.get_expr(), code_sz, code));
+        m_decls.set(idx, vm_decl(n, idx, d.get_expr(), code_sz, code));
     }
 
     void initialize() {
         if (!m_initialized) {
             m_initialized = true;
             g_vm_builtins->for_each([&](name const & n, pair<unsigned, vm_function> const & p) {
-                    add(vm_decl(n, p.first, p.second));
+                    add(vm_decl(n, m_decls.size(), p.first, p.second));
                 });
         }
     }
diff --git a/src/library/vm.h b/src/library/vm.h
index 8ae1d399a0..d02ea4f30a 100644
--- a/src/library/vm.h
+++ b/src/library/vm.h
@@ -314,6 +314,7 @@ struct vm_decl_cell {
     MK_LEAN_RC();
     bool       m_builtin;
     name       m_name;
+    unsigned   m_idx;
     expr       m_expr;
     unsigned   m_arity;
     union {
@@ -324,8 +325,8 @@ struct vm_decl_cell {
         vm_function    m_fn;
     };
 
-    vm_decl_cell(name const & n, unsigned arity, vm_function fn);
-    vm_decl_cell(name const & n, expr const & e, unsigned code_sz, vm_instr const * code);
+    vm_decl_cell(name const & n, unsigned idx, unsigned arity, vm_function fn);
+    vm_decl_cell(name const & n, unsigned idx, expr const & e, unsigned code_sz, vm_instr const * code);
     ~vm_decl_cell();
     void dealloc();
 };
@@ -336,10 +337,10 @@ class vm_decl {
     explicit vm_decl(vm_decl_cell * ptr):m_ptr(ptr) { if (m_ptr) m_ptr->inc_ref(); }
 public:
     vm_decl():m_ptr(nullptr) {}
-    vm_decl(name const & n, unsigned arity, vm_function fn):
-        vm_decl(new vm_decl_cell(n, arity, fn)) {}
-    vm_decl(name const & n, expr const & e, unsigned code_sz, vm_instr const * code):
-        vm_decl(new vm_decl_cell(n, e, code_sz, code)) {}
+    vm_decl(name const & n, unsigned idx, unsigned arity, vm_function fn):
+        vm_decl(new vm_decl_cell(n, idx, arity, fn)) {}
+    vm_decl(name const & n, unsigned idx, expr const & e, unsigned code_sz, vm_instr const * code):
+        vm_decl(new vm_decl_cell(n, idx, e, code_sz, code)) {}
     vm_decl(vm_decl const & s):m_ptr(s.m_ptr) { if (m_ptr) m_ptr->inc_ref(); }
     vm_decl(vm_decl && s):m_ptr(s.m_ptr) { s.m_ptr = nullptr; }
     ~vm_decl() { if (m_ptr) m_ptr->dec_ref(); }
@@ -350,6 +351,7 @@ public:
     vm_decl & operator=(vm_decl && s) { LEAN_MOVE_REF(s); }
 
     bool is_builtin() const { lean_assert(m_ptr); return m_ptr->m_builtin; }
+    unsigned get_idx() const { lean_assert(m_ptr); return m_ptr->m_idx; }
     name get_name() const { lean_assert(m_ptr); return m_ptr->m_name; }
     unsigned get_arity() const { lean_assert(m_ptr); return m_ptr->m_arity; }
     unsigned get_code_size() const { lean_assert(!is_builtin()); return m_ptr->m_code_size; }