diff --git a/src/library/compiler/emit_bytecode.cpp b/src/library/compiler/emit_bytecode.cpp
index 49f6242984..51528cc53a 100644
--- a/src/library/compiler/emit_bytecode.cpp
+++ b/src/library/compiler/emit_bytecode.cpp
@@ -102,8 +102,7 @@ class emit_bytecode_fn {
         buffer<expr> args;
         expr fn = get_app_args(e, args);
         lean_assert(is_constant(fn));
-        name const & fn_name = const_name(fn);
-        unsigned num = get_vm_supported_cases_num_minors(m_env, fn);
+        unsigned num = *is_internal_cases(fn);
         lean_assert(args.size() == num + 1);
         lean_assert(num >= 1);
         /** compile major premise */
@@ -112,14 +111,7 @@ class emit_bytecode_fn {
         buffer<unsigned> cases_args;
         buffer<unsigned> goto_pcs;
         cases_args.resize(num, 0);
-        if (fn_name == get_nat_cases_on_name()) {
-            emit(mk_nat_cases_instr(0, 0));
-        } else if (optional<unsigned> builtin_cases_idx = get_vm_builtin_cases_idx(m_env, fn_name)) {
-            #if defined(__GNUC__) && !defined(__CLANG__)
-            #pragma GCC diagnostic ignored "-Wmaybe-uninitialized"
-            #endif
-            emit(mk_builtin_cases_instr(*builtin_cases_idx, cases_args.size(), cases_args.data()));
-        } else if (num == 1) {
+        if (num == 1) {
             emit(mk_destruct_instr());
         } else if (num == 2) {
             emit(mk_cases2_instr(0, 0));
@@ -150,7 +142,7 @@ class emit_bytecode_fn {
             }
         }
         /* Fix cases instruction pc's */
-        if (num >= 2 || get_vm_builtin_cases_idx(m_env, fn_name)) {
+        if (num >= 2) {
             for (unsigned i = 0; i < cases_args.size(); i++)
                 m_code[cases_pos].set_pc(i, cases_args[i]);
         }
@@ -204,7 +196,7 @@ class emit_bytecode_fn {
 
     void compile_app(expr const & e, unsigned bpz, name_map<unsigned> const & m) {
         expr const & fn = get_app_fn(e);
-        if (is_vm_supported_cases(m_env, fn)) {
+        if (is_internal_cases(fn)) {
             compile_cases_on(e, bpz, m);
         } else if (is_internal_cnstr(fn)) {
             compile_cnstr(e, bpz, m);
diff --git a/src/library/compiler/simp_inductive.cpp b/src/library/compiler/simp_inductive.cpp
index 803e85f556..384582b03e 100644
--- a/src/library/compiler/simp_inductive.cpp
+++ b/src/library/compiler/simp_inductive.cpp
@@ -43,29 +43,6 @@ optional<unsigned> is_internal_cases(expr const & e) {
     return is_internal_symbol(e, *g_cases);
 }
 
-bool is_vm_supported_cases(environment const & env, expr const & e) {
-    return
-        is_internal_cases(e) ||
-        is_constant(e, get_nat_cases_on_name()) ||
-        (is_constant(e) && get_vm_builtin_cases_idx(env, const_name(e)));
-}
-
-unsigned get_vm_supported_cases_num_minors(environment const & env, expr const & fn) {
-    name const & fn_name = const_name(fn);
-    if (fn_name == get_nat_cases_on_name()) {
-        return 2;
-    } else {
-        optional<unsigned> builtin_cases_idx = get_vm_builtin_cases_idx(env, fn_name);
-        if (builtin_cases_idx) {
-            name const & I_name = fn_name.get_prefix();
-            return get_num_constructors(env, I_name);
-        } else {
-            lean_assert(is_internal_cases(fn));
-            return *is_internal_cases(fn);
-        }
-    }
-}
-
 class simp_inductive_fn {
     type_checker::state  m_st;
     local_ctx            m_lctx;
diff --git a/src/library/compiler/simp_inductive.h b/src/library/compiler/simp_inductive.h
index 45fd3a60ca..e0371667a0 100644
--- a/src/library/compiler/simp_inductive.h
+++ b/src/library/compiler/simp_inductive.h
@@ -19,14 +19,6 @@ optional<unsigned> is_internal_cnstr(expr const & e);
 /** \brief Return non-none n iff \c e is of the form _cases.n */
 optional<unsigned> is_internal_cases(expr const & e);
 
-/** \brief Return true iff 'e' is an internal cases, a nat.cases_on,
-    or a VM builtin cases. That is, it returns true for constants
-    that produce branching during code generation. */
-bool is_vm_supported_cases(environment const & env, expr const & e);
-
-/** \brief Return the number of minor premises for a vm supported cases construct. */
-unsigned get_vm_supported_cases_num_minors(environment const & env, expr const & fn);
-
 void initialize_simp_inductive();
 void finalize_simp_inductive();
 }
diff --git a/src/library/vm/optimize.cpp b/src/library/vm/optimize.cpp
index edc6dd9eac..edd72d22d8 100644
--- a/src/library/vm/optimize.cpp
+++ b/src/library/vm/optimize.cpp
@@ -109,11 +109,11 @@ class live_vars_fn {
             s = collect(pc+1);
             s.insert(instr.get_idx());
             break;
-        case opcode::Cases2: case opcode::NatCases:
+        case opcode::Cases2:
             s = collect(instr.get_cases2_pc(0));
             s.merge(collect(instr.get_cases2_pc(1)));
             break;
-        case opcode::CasesN: case opcode::BuiltinCases:
+        case opcode::CasesN:
             s = collect(instr.get_casesn_pc(0));
             for (unsigned i = 1; i < instr.get_casesn_size(); i++)
                 s.merge(collect(instr.get_casesn_pc(i)));
diff --git a/src/library/vm/vm.cpp b/src/library/vm/vm.cpp
index dc2c5aeaf7..4596f2f300 100644
--- a/src/library/vm/vm.cpp
+++ b/src/library/vm/vm.cpp
@@ -521,10 +521,6 @@ static void display_fn(std::ostream & out, unsigned fn_idx) {
         out << fn_idx;
 }
 
-static void display_builtin_cases(std::ostream & out, unsigned cases_idx) {
-    display_fn(out, cases_idx);
-}
-
 void vm_instr::display(std::ostream & out) const {
     switch (m_op) {
     case opcode::Push:          out << "push " << m_idx; break;
@@ -544,14 +540,6 @@ void vm_instr::display(std::ostream & out) const {
         for (unsigned i = 0; i < get_casesn_size(); i++)
             out << " " << get_casesn_pc(i);
         break;
-    case opcode::BuiltinCases:
-        out << "builtin_cases ";
-        display_builtin_cases(out, get_cases_idx());
-        out << ",";
-        for (unsigned i = 0; i < get_casesn_size(); i++)
-            out << " " << get_casesn_pc(i);
-        break;
-    case opcode::NatCases:      out << "nat_cases " << m_pc[1]; break;
     case opcode::Proj:          out << "proj " << m_idx; break;
     case opcode::Apply:         out << "apply"; break;
     case opcode::InvokeGlobal:
@@ -582,9 +570,9 @@ unsigned vm_instr::get_num_pcs() const {
     switch (m_op) {
     case opcode::Goto:
         return 1;
-    case opcode::Cases2: case opcode::NatCases:
+    case opcode::Cases2:
         return 2;
-    case opcode::CasesN: case opcode::BuiltinCases:
+    case opcode::CasesN:
         return get_casesn_size();
     default:
         return 0;
@@ -595,9 +583,9 @@ unsigned vm_instr::get_pc(unsigned i) const {
     lean_assert(i < get_num_pcs());
     switch (m_op) {
     case opcode::Goto:
-    case opcode::Cases2: case opcode::NatCases:
+    case opcode::Cases2:
         return m_pc[i];
-    case opcode::CasesN: case opcode::BuiltinCases:
+    case opcode::CasesN:
         return get_casesn_pc(i);
     default:
         lean_unreachable();
@@ -608,10 +596,10 @@ void vm_instr::set_pc(unsigned i, unsigned pc) {
     lean_assert(i < get_num_pcs());
     switch (m_op) {
     case opcode::Goto:
-    case opcode::Cases2: case opcode::NatCases:
+    case opcode::Cases2:
         m_pc[i] = pc;
         break;
-    case opcode::CasesN: case opcode::BuiltinCases:
+    case opcode::CasesN:
         set_casesn_pc(i, pc);
         break;
     default:
@@ -701,13 +689,6 @@ vm_instr mk_unreachable_instr() { return vm_instr(opcode::Unreachable); }
 
 vm_instr mk_apply_instr() { return vm_instr(opcode::Apply); }
 
-vm_instr mk_nat_cases_instr(unsigned pc1, unsigned pc2) {
-    vm_instr r(opcode::NatCases);
-    r.m_pc[0] = pc1;
-    r.m_pc[1] = pc2;
-    return r;
-}
-
 vm_instr mk_cases2_instr(unsigned pc1, unsigned pc2) {
     vm_instr r(opcode::Cases2);
     r.m_pc[0] = pc1;
@@ -718,7 +699,6 @@ vm_instr mk_cases2_instr(unsigned pc1, unsigned pc2) {
 vm_instr mk_casesn_instr(unsigned num_pc, unsigned const * pcs) {
     lean_assert(num_pc >= 2);
     vm_instr r(opcode::CasesN);
-    r.m_cases_idx = 0; /* not really needed, but it avoids a valgrind warning. */
     r.m_npcs = new unsigned[num_pc + 1];
     r.m_npcs[0] = num_pc;
     for (unsigned i = 0; i < num_pc; i++)
@@ -726,16 +706,6 @@ vm_instr mk_casesn_instr(unsigned num_pc, unsigned const * pcs) {
     return r;
 }
 
-vm_instr mk_builtin_cases_instr(unsigned cases_idx, unsigned num_pc, unsigned const * pcs) {
-    vm_instr r(opcode::BuiltinCases);
-    r.m_cases_idx = cases_idx;
-    r.m_npcs      = new unsigned[num_pc + 1];
-    r.m_npcs[0]   = num_pc;
-    for (unsigned i = 0; i < num_pc; i++)
-        r.m_npcs[i+1] = pcs[i];
-    return r;
-}
-
 vm_instr mk_invoke_global_instr(unsigned fn_idx) {
     vm_instr r(opcode::InvokeGlobal);
     r.m_fn_idx = fn_idx;
@@ -764,7 +734,6 @@ vm_instr mk_closure_instr(unsigned fn_idx, unsigned n) {
 void vm_instr::release_memory() {
     switch (m_op) {
     case opcode::CasesN:
-    case opcode::BuiltinCases:
         delete[] m_npcs;
         break;
     case opcode::Num:
@@ -802,16 +771,14 @@ void vm_instr::copy_args(vm_instr const & i) {
     case opcode::Goto:
         m_pc[0] = i.m_pc[0];
         break;
-    case opcode::Cases2: case opcode::NatCases:
+    case opcode::Cases2:
         m_pc[0] = i.m_pc[0];
         m_pc[1] = i.m_pc[1];
         break;
     case opcode::CasesN:
-    case opcode::BuiltinCases:
         m_npcs = new unsigned[i.m_npcs[0] + 1];
         for (unsigned j = 0; j < i.m_npcs[0] + 1; j++)
             m_npcs[j] = i.m_npcs[j];
-        m_cases_idx = i.m_cases_idx;
         break;
     case opcode::SConstructor:
         m_cidx = i.m_cidx;
@@ -855,9 +822,8 @@ vm_instr::vm_instr(vm_instr && i):
         m_str    = i.m_str;
         i.m_str  = nullptr;
         break;
-    case opcode::CasesN: case opcode::BuiltinCases:
+    case opcode::CasesN:
         m_npcs      = i.m_npcs;
-        m_cases_idx = i.m_cases_idx;
         i.m_npcs    = nullptr;
         break;
     default:
@@ -889,8 +855,7 @@ vm_instr & vm_instr::operator=(vm_instr && s) {
         m_str    = s.m_str;
         s.m_str  = nullptr;
         break;
-    case opcode::CasesN: case opcode::BuiltinCases:
-        m_cases_idx = s.m_cases_idx;
+    case opcode::CasesN:
         m_npcs      = s.m_npcs;
         s.m_npcs    = nullptr;
         break;
@@ -919,13 +884,10 @@ void vm_instr::serialize(serializer & s, std::function<name(unsigned)> const & i
     case opcode::Goto:
         s << m_pc[0];
         break;
-    case opcode::Cases2: case opcode::NatCases:
+    case opcode::Cases2:
         s << m_pc[0];
         s << m_pc[1];
         break;
-    case opcode::BuiltinCases:
-        s << idx2name(m_cases_idx);
-        /* fall-thru */
     case opcode::CasesN:
         s << m_npcs[0];
         for (unsigned j = 1; j < m_npcs[0] + 1; j++)
@@ -993,20 +955,11 @@ static vm_instr read_vm_instr(deserializer & d) {
     case opcode::Cases2:
         pc = d.read_unsigned();
         return mk_cases2_instr(pc, d.read_unsigned());
-    case opcode::NatCases:
-        pc = d.read_unsigned();
-        return mk_nat_cases_instr(pc, d.read_unsigned());
     case opcode::CasesN: {
         buffer<unsigned> pcs;
         read_cases_pcs(d, pcs);
         return mk_casesn_instr(pcs.size(), pcs.data());
     }
-    case opcode::BuiltinCases: {
-        idx = get_vm_index(read_name(d));
-        buffer<unsigned> pcs;
-        read_cases_pcs(d, pcs);
-        return mk_builtin_cases_instr(idx, pcs.size(), pcs.data());
-    }
     case opcode::SConstructor:
         return mk_sconstructor_instr(d.read_unsigned());
     case opcode::Constructor:
@@ -1065,7 +1018,6 @@ void vm_decl_cell::dealloc() {
 /** \brief VM builtin functions */
 static name_map<std::tuple<unsigned, char const *, vm_function>> * g_vm_builtins = nullptr;
 static name_map<std::tuple<unsigned, char const *, vm_cfunction>> * g_vm_cbuiltins = nullptr;
-static name_map<std::tuple<char const *, vm_cases_function>> * g_vm_cases_builtins = nullptr;
 static bool g_may_update_vm_builtins = true;
 
 void declare_vm_builtin(name const & n, char const * i, unsigned arity, vm_function fn) {
@@ -1124,26 +1076,16 @@ void declare_vm_builtin(name const & n, char const * i, unsigned arity, vm_cfunc
 }
 
 bool is_vm_builtin_function(name const & fn) {
-    return g_vm_builtins->contains(fn) || g_vm_cbuiltins->contains(fn) || g_vm_cases_builtins->contains(fn);
-}
-
-void declare_vm_cases_builtin(name const & n, char const * i, vm_cases_function fn) {
-    lean_assert(g_may_update_vm_builtins);
-    g_vm_cases_builtins->insert(n, std::make_tuple(i, fn));
+    return g_vm_builtins->contains(fn) || g_vm_cbuiltins->contains(fn);
 }
 
 /** \brief VM function/constant declarations are stored in an environment extension. */
 struct vm_decls : public environment_extension {
     unsigned_map<vm_decl>           m_decls;
-    unsigned_map<vm_cases_function> m_cases;
 
     name                            m_monitor;
 
     vm_decls() {
-        g_vm_cases_builtins->for_each([&](name const & n, std::tuple<char const *, vm_cases_function> const & p) {
-                unsigned idx = get_vm_index(n);
-                m_cases.insert(idx, std::get<1>(p));
-            });
         g_vm_builtins->for_each([&](name const & n, std::tuple<unsigned, char const *, vm_function> const & p) {
                 add_core(vm_decl(n, get_vm_index(n), std::get<0>(p), std::get<2>(p)));
             });
@@ -1395,15 +1337,6 @@ optional<vm_decl> get_vm_decl(environment const & env, name const & n) {
         return optional<vm_decl>();
 }
 
-optional<unsigned> get_vm_builtin_cases_idx(environment const & env, name const & n) {
-    vm_decls const & ext = get_extension(env);
-    auto idx = get_vm_index(n);
-    if (ext.m_cases.contains(idx))
-        return optional<unsigned>(idx);
-    else
-        return optional<unsigned>();
-}
-
 constexpr unsigned g_null_fn_idx = -1;
 
 static name * g_debugger = nullptr;
@@ -1421,8 +1354,6 @@ vm_state::vm_state(environment const & env, options const & opts):
     m_options(opts),
     m_decl_map(get_extension(m_env).m_decls),
     m_decl_vector(get_vm_index_bound()),
-    m_builtin_cases_map(get_extension(m_env).m_cases),
-    m_builtin_cases_vector(get_vm_index_bound()),
     m_code(nullptr),
     m_fn_idx(g_null_fn_idx),
     m_bp(0) {
@@ -1446,19 +1377,6 @@ vm_decl const & vm_state::get_decl(unsigned idx) const {
     return m_decl_vector[idx];
 }
 
-vm_cases_function const & vm_state::get_builtin_cases(unsigned idx) const {
-    lean_assert(idx < m_builtin_cases_vector.size());
-    vm_cases_function const & fn = m_builtin_cases_vector[idx];
-    if (fn != nullptr) return fn;
-    if (auto fn_ = m_builtin_cases_map.find(idx)) {
-        const_cast<vm_state *>(this)->m_builtin_cases_vector[idx] = *fn_;
-    } else {
-        lean_unreachable();
-    }
-    return m_builtin_cases_vector[idx];
-}
-
-
 struct vm_state::debugger_state {
     vm_state m_vm;
     vm_obj   m_state;
@@ -1512,7 +1430,6 @@ void vm_state::update_env(environment const & env) {
     m_decl_map    = ext.m_decls;
     m_decl_vector.resize(get_vm_index_bound());
     m_was_updated = true;
-    lean_assert(is_eqp(m_builtin_cases_map, ext.m_cases));
 }
 
 void vm_state::push_fields(vm_obj const & obj) {
@@ -3053,45 +2970,6 @@ void vm_state::run() {
             m_pc = instr.get_cases2_pc(cidx(top));
             goto main_loop;
         }
-        case opcode::NatCases: {
-            /** Instruction: natcases pc1 pc2
-
-                stack before,              after (if n = 0)    after (if n > 0)
-                ...                        ...                 ...
-                v                 ==>      v                   v
-                n                                              n-1
-
-                m_pc := pc1  if  n == 0
-                := pc2  if  otherwise
-            */
-            vm_obj & top = m_stack.back();
-            if (is_simple(top)) {
-                unsigned val = cidx(top);
-                if (val == 0) {
-                    stack_pop_back();
-                    m_pc++;
-                    goto main_loop;
-                } else {
-                    vm_obj new_value = mk_vm_simple(val - 1);
-                    swap(top, new_value);
-                    m_pc = instr.get_cases2_pc(1);
-                    goto main_loop;
-                }
-            } else {
-                /* to_mpz checks lean_vm_check(is_mpz(top)) */
-                mpz const & val = to_mpz(top);
-                if (val == 0) {
-                    stack_pop_back();
-                    m_pc++;
-                    goto main_loop;
-                } else {
-                    vm_obj new_value = mk_vm_mpz(val - 1);
-                    swap(top, new_value);
-                    m_pc = instr.get_cases2_pc(1);
-                    goto main_loop;
-                }
-            }
-        }
         case opcode::CasesN: {
             /** Instruction: casesn pc_0 ... pc_[n-1]
 
@@ -3110,19 +2988,6 @@ void vm_state::run() {
             m_pc = instr.get_casesn_pc(cidx(top));
             goto main_loop;
         }
-        case opcode::BuiltinCases: {
-            /** Instruction: builtin_cases
-                It is similar to CasesN, but uses the vm_cases_function to extract the data.
-            */
-            vm_obj top = m_stack.back();
-            stack_pop_back();
-            vm_cases_function fn = get_builtin_cases(instr.get_cases_idx());
-            buffer<vm_obj> data;
-            unsigned cidx = fn(top, data);
-            std::copy(data.begin(), data.end(), std::back_inserter(m_stack));
-            m_pc = instr.get_casesn_pc(cidx);
-            goto main_loop;
-        }
         case opcode::Proj: {
             /** Instruction: proj i
 
@@ -3623,8 +3488,6 @@ char const * get_vm_builtin_internal_name(name const & fn) {
         return std::get<1>(*p);
     if (auto p = g_vm_cbuiltins->find(fn))
         return std::get<1>(*p);
-    if (auto p = g_vm_cases_builtins->find(fn))
-        return std::get<0>(*p);
     return nullptr;
 }
 
@@ -3633,8 +3496,6 @@ vm_builtin_kind get_vm_builtin_kind(name const & fn) {
         return vm_builtin_kind::VMFun;
     if (g_vm_cbuiltins->contains(fn))
         return vm_builtin_kind::CFun;
-    if (g_vm_cases_builtins->contains(fn))
-        return vm_builtin_kind::Cases;
     lean_unreachable();
 }
 
@@ -3715,7 +3576,6 @@ void initialize_vm_core() {
     g_vm_index_manager = new vm_index_manager;
     g_vm_builtins = new name_map<std::tuple<unsigned, char const *, vm_function>>();
     g_vm_cbuiltins = new name_map<std::tuple<unsigned, char const *, vm_cfunction>>();
-    g_vm_cases_builtins = new name_map<std::tuple<char const *, vm_cases_function>>();
     g_may_update_vm_builtins = true;
     DEBUG_CODE({
             /* We only trace VM in debug mode because it produces a 10% performance penalty */
@@ -3727,7 +3587,6 @@ void initialize_vm_core() {
 void finalize_vm_core() {
     delete g_vm_builtins;
     delete g_vm_cbuiltins;
-    delete g_vm_cases_builtins;
     delete g_vm_index_manager;
 }
 
diff --git a/src/library/vm/vm.h b/src/library/vm/vm.h
index 26649b124a..f89ca9c4a6 100644
--- a/src/library/vm/vm.h
+++ b/src/library/vm/vm.h
@@ -305,17 +305,13 @@ class vm_state;
 /** Builtin functions that take arguments from the VM stack. */
 typedef void (*vm_function)(vm_state & s);
 
-/** Custom 'cases' operators. Given an object \c o, it returns the constructor index and stores
-    the data stored in the object in the buffer \c data. */
-typedef unsigned (*vm_cases_function)(vm_obj const & o, buffer<vm_obj> & data);
-
 typedef pair<name, optional<expr>> vm_local_info;
 
 /** \brief VM instruction opcode */
 enum class opcode {
     Push, Move, Ret, Drop, Goto,
     SConstructor, Constructor, Num, String,
-    Destruct, Cases2, CasesN, NatCases, BuiltinCases, Proj,
+    Destruct, Cases2, CasesN, Proj,
     Apply, InvokeGlobal, InvokeBuiltin, InvokeCFun,
     Closure, Unreachable, Expr, LocalInfo
 };
@@ -332,13 +328,12 @@ class vm_instr {
         unsigned m_idx;
         /* Drop */
         unsigned m_num;
-        /* Goto, Cases2 and NatCases */
+        /* Goto and Cases2 */
         struct {
             unsigned m_pc[2];
         };
-        /* CasesN and BuiltinCases */
+        /* CasesN */
         struct {
-            unsigned   m_cases_idx; /* only used for BuiltinCases */
             unsigned * m_npcs;
         };
         /* Constructor, SConstructor */
@@ -371,10 +366,8 @@ class vm_instr {
     friend vm_instr mk_ret_instr();
     friend vm_instr mk_destruct_instr();
     friend vm_instr mk_unreachable_instr();
-    friend vm_instr mk_nat_cases_instr(unsigned pc1, unsigned pc2);
     friend vm_instr mk_cases2_instr(unsigned pc1, unsigned pc2);
     friend vm_instr mk_casesn_instr(unsigned num_pc, unsigned const * pcs);
-    friend vm_instr mk_builtin_cases_instr(unsigned cases_idx, unsigned num_pc, unsigned const * pcs);
     friend vm_instr mk_apply_instr();
     friend vm_instr mk_invoke_global_instr(unsigned fn_idx);
     friend vm_instr mk_invoke_cfun_instr(unsigned fn_idx);
@@ -429,35 +422,30 @@ public:
     }
 
     unsigned get_cases2_pc(unsigned i) const {
-        lean_assert(m_op == opcode::Cases2 || m_op == opcode::NatCases);
+        lean_assert(m_op == opcode::Cases2);
         lean_vm_check(i < 2);
         return m_pc[i];
     }
 
     void set_cases2_pc(unsigned i, unsigned pc) {
-        lean_assert(m_op == opcode::Cases2 || m_op == opcode::NatCases);
+        lean_assert(m_op == opcode::Cases2);
         lean_vm_check(i < 2);
         m_pc[i] = pc;
     }
 
-    unsigned get_cases_idx() const {
-        lean_assert(m_op == opcode::BuiltinCases);
-        return m_cases_idx;
-    }
-
     unsigned get_casesn_size() const {
-        lean_assert(m_op == opcode::CasesN || m_op == opcode::BuiltinCases);
+        lean_assert(m_op == opcode::CasesN);
         return m_npcs[0];
     }
 
     unsigned get_casesn_pc(unsigned i) const {
-        lean_assert(m_op == opcode::CasesN || m_op == opcode::BuiltinCases);
+        lean_assert(m_op == opcode::CasesN);
         lean_vm_check(i < get_casesn_size());
         return m_npcs[i+1];
     }
 
     void set_casesn_pc(unsigned i, unsigned pc) const {
-        lean_assert(m_op == opcode::CasesN || m_op == opcode::BuiltinCases);
+        lean_assert(m_op == opcode::CasesN);
         lean_vm_check(i < get_casesn_size());
         m_npcs[i+1] = pc;
     }
@@ -518,10 +506,8 @@ vm_instr mk_string_instr(std::string const & v);
 vm_instr mk_ret_instr();
 vm_instr mk_destruct_instr();
 vm_instr mk_unreachable_instr();
-vm_instr mk_nat_cases_instr(unsigned pc1, unsigned pc2);
 vm_instr mk_cases2_instr(unsigned pc1, unsigned pc2);
 vm_instr mk_casesn_instr(unsigned num_pc, unsigned const * pcs);
-vm_instr mk_builtin_cases_instr(unsigned cases_idx, unsigned num_pc, unsigned const * pcs);
 vm_instr mk_apply_instr();
 vm_instr mk_invoke_global_instr(unsigned fn_idx);
 vm_instr mk_invoke_cfun_instr(unsigned fn_idx);
@@ -614,15 +600,11 @@ public:
     typedef std::vector<vm_decl> decl_vector;
     typedef std::vector<optional<vm_obj>> cache_vector;
     typedef unsigned_map<vm_decl> decl_map;
-    typedef std::vector<vm_cases_function> builtin_cases_vector;
-    typedef unsigned_map<vm_cases_function> builtin_cases_map;
     environment                 m_env;
     options                     m_options;
     decl_map                    m_decl_map;
     decl_vector                 m_decl_vector;
     cache_vector                m_cache_vector; /* for 0-ary declarations */
-    builtin_cases_map           m_builtin_cases_map;
-    builtin_cases_vector        m_builtin_cases_vector;
     vm_instr const *            m_code;   /* code of the current function being executed */
     unsigned                    m_fn_idx; /* function idx being executed */
     unsigned                    m_pc;     /* program counter */
@@ -676,8 +658,6 @@ public:
 
     vm_decl const & get_decl(unsigned idx) const;
 
-    vm_cases_function const & get_builtin_cases(unsigned idx) const;
-
 public:
     vm_state(environment const & env, options const & opts);
     ~vm_state();
@@ -891,14 +871,6 @@ void declare_vm_builtin(name const & n, char const * internal_name, unsigned ari
 
 #define DECLARE_VM_BUILTIN(n, fn) declare_vm_builtin(n, #fn, fn)
 
-/** \brief Add builtin implementation for a cases_on */
-void declare_vm_cases_builtin(name const & n, char const * internal_name, vm_cases_function fn);
-
-#define DECLARE_VM_CASES_BUILTIN(n, fn) declare_vm_cases_builtin(n, #fn, fn)
-
-/** \brief Return builtin cases internal index. */
-optional<unsigned> get_vm_builtin_cases_idx(environment const & env, name const & n);
-
 /** Register in the given environment \c fn as the implementation for function \c n.
     These APIs should be used when we dynamically load native code stored in a shared object (aka DLL)
     that implements lean functions. */
@@ -958,7 +930,7 @@ bool is_vm_builtin_function(name const & fn);
     Return nullptr if \c fn is not a builtin. */
 char const * get_vm_builtin_internal_name(name const & fn);
 
-enum class vm_builtin_kind { VMFun, CFun, Cases };
+enum class vm_builtin_kind { VMFun, CFun };
 
 /** \brief Return the kind of a builtin function.
     \pre is_vm_builtin_function(fn) */