diff --git a/examples/riscv/kernel-trap-entry/Holmakefile b/examples/riscv/kernel-trap-entry/Holmakefile
deleted file mode 100644
index d79e4e0a2..000000000
--- a/examples/riscv/kernel-trap-entry/Holmakefile
+++ /dev/null
@@ -1,30 +0,0 @@
-INCLUDES = $(HOLDIR)/examples/l3-machine-code/common \
-           $(HOLDIR)/examples/l3-machine-code/arm8/model \
-           $(HOLDIR)/examples/l3-machine-code/arm8/step \
-           $(HOLDIR)/examples/l3-machine-code/m0/model \
-           $(HOLDIR)/examples/l3-machine-code/m0/step \
-           $(HOLBADIR)/src/shared/l3-machine-code/riscv/model \
-           $(HOLBADIR)/src/shared/l3-machine-code/riscv/step \
-           $(HOLBADIR)/src/theory/bir \
-           $(HOLBADIR)/src/theory/bir-support \
-           $(HOLBADIR)/src/theory/program_logic \
-           $(HOLBADIR)/src/theory/tools/lifter \
-           $(HOLBADIR)/src/theory/tools/backlifter \
-           $(HOLBADIR)/src/tools/lifter \
-           $(HOLBADIR)/src/tools/backlifter \
-           $(HOLBADIR)/src/tools/exec \
-           $(HOLBADIR)/src/tools/comp \
-           $(HOLBADIR)/src/tools/wp \
-           $(HOLBADIR)/src/tools/backlifter \
-           $(HOLBADIR)/src/tools/symbexec \
-           $(HOLBADIR)/src/tools/symbexec/examples/common \
-           $(HOLBADIR)/src
-
-all: $(DEFAULT_TARGETS)
-.PHONY: all
-
-ifdef POLY
-ifndef HOLBA_POLYML_HEAPLESS
-HOLHEAP = $(HOLBADIR)/src/holba-heap
-endif
-endif
diff --git a/examples/riscv/kernel-trap-entry/kernel.da b/examples/riscv/kernel-trap-entry/kernel.da
deleted file mode 100644
index 51405f6dd..000000000
--- a/examples/riscv/kernel-trap-entry/kernel.da
+++ /dev/null
@@ -1,52 +0,0 @@
-
-build/qemu_virt_norvc/kernel.elf:     file format elf64-littleriscv
-
-
-Disassembly of section .text:
-
-00000000800000e0 <trap_entry>:
-    800000e0:	34051573          	csrrw	a0,mscratch,a0
-    800000e4:	00153823          	sd	ra,16(a0)
-    800000e8:	00253c23          	sd	sp,24(a0)
-    800000ec:	02353023          	sd	gp,32(a0)
-    800000f0:	02453423          	sd	tp,40(a0)
-    800000f4:	02553823          	sd	t0,48(a0)
-    800000f8:	02653c23          	sd	t1,56(a0)
-    800000fc:	04753023          	sd	t2,64(a0)
-    80000100:	04853423          	sd	s0,72(a0)
-    80000104:	04953823          	sd	s1,80(a0)
-    80000108:	06b53023          	sd	a1,96(a0)
-    8000010c:	06c53423          	sd	a2,104(a0)
-    80000110:	06d53823          	sd	a3,112(a0)
-    80000114:	06e53c23          	sd	a4,120(a0)
-    80000118:	08f53023          	sd	a5,128(a0)
-    8000011c:	09053423          	sd	a6,136(a0)
-    80000120:	09153823          	sd	a7,144(a0)
-    80000124:	09253c23          	sd	s2,152(a0)
-    80000128:	0b353023          	sd	s3,160(a0)
-    8000012c:	0b453423          	sd	s4,168(a0)
-    80000130:	0b553823          	sd	s5,176(a0)
-    80000134:	0b653c23          	sd	s6,184(a0)
-    80000138:	0d753023          	sd	s7,192(a0)
-    8000013c:	0d853423          	sd	s8,200(a0)
-    80000140:	0d953823          	sd	s9,208(a0)
-    80000144:	0da53c23          	sd	s10,216(a0)
-    80000148:	0fb53023          	sd	s11,224(a0)
-    8000014c:	0fc53423          	sd	t3,232(a0)
-    80000150:	0fd53823          	sd	t4,240(a0)
-    80000154:	0fe53c23          	sd	t5,248(a0)
-    80000158:	11f53023          	sd	t6,256(a0)
-    8000015c:	34102373          	csrr	t1,mepc
-    80000160:	340023f3          	csrr	t2,mscratch
-    80000164:	00653423          	sd	t1,8(a0)
-    80000168:	04753c23          	sd	t2,88(a0)
-    8000016c:	00005197          	auipc	gp,0x5
-    80000170:	69818193          	addi	gp,gp,1688 # 80005804 <__global_pointer$>
-    80000174:	00006117          	auipc	sp,0x6
-    80000178:	28c10113          	addi	sp,sp,652 # 80006400 <slots>
-    8000017c:	f14022f3          	csrr	t0,mhartid
-    80000180:	00a29293          	slli	t0,t0,0xa
-    80000184:	40510133          	sub	sp,sp,t0
-    80000188:	342025f3          	csrr	a1,mcause
-    8000018c:	34302673          	csrr	a2,mtval
-    80000190:	238040ef          	jal	800043c8 <trap_handler>
diff --git a/examples/riscv/kernel-trap-entry/kernelScript.sml b/examples/riscv/kernel-trap-entry/kernelScript.sml
deleted file mode 100644
index aa96c12a8..000000000
--- a/examples/riscv/kernel-trap-entry/kernelScript.sml
+++ /dev/null
@@ -1,21 +0,0 @@
-open HolKernel Parse;
-
-open bir_lifter_interfaceLib;
-open birs_auxLib;
-
-val _ = Parse.current_backend := PPBackEnd.vt100_terminal;
-val _ = set_trace "bir_inst_lifting.DEBUG_LEVEL" 2;
-
-val _ = new_theory "kernel";
-
-val _ = lift_da_and_store "kernel" "kernel.da" da_riscv
- ((Arbnum.fromInt 0x800000e0), (Arbnum.fromInt 0x80000194));
-
-(* ----------------------------------------- *)
-(* Program variable definitions and theorems *)
-(* ----------------------------------------- *)
-
-val bir_prog_def = DB.fetch "-" "bir_kernel_prog_def";
-val _ = gen_prog_vars_birenvtyl_defthms "kernel" bir_prog_def;
-
-val _ = export_theory ();