diff --git a/repos/base-sel4/src/core/platform_pd.cc b/repos/base-sel4/src/core/platform_pd.cc
index 18fe3ab90..32846a356 100644
--- a/repos/base-sel4/src/core/platform_pd.cc
+++ b/repos/base-sel4/src/core/platform_pd.cc
@@ -79,7 +79,13 @@ bool Platform_pd::bind_thread(Platform_thread *thread)
 
 void Platform_pd::unbind_thread(Platform_thread *thread)
 {
-	PDBG("not implemented");
+	if (!thread)
+		return;
+
+	if (thread->_utcb)
+		_vm_space.unmap(thread->_utcb, 1);
+	else
+		_vm_space.unmap(thread->INITIAL_IPC_BUFFER_VIRT, 1);
 }
 
 
diff --git a/repos/base-sel4/src/core/platform_thread.cc b/repos/base-sel4/src/core/platform_thread.cc
index b084d3646..6fcfdddb3 100644
--- a/repos/base-sel4/src/core/platform_thread.cc
+++ b/repos/base-sel4/src/core/platform_thread.cc
@@ -217,7 +217,10 @@ Platform_thread::Platform_thread(size_t, const char *name, unsigned priority,
 
 Platform_thread::~Platform_thread()
 {
-	PDBG("not completely implemented");
+	if (_pd) {
+		seL4_TCB_Suspend(_info.tcb_sel.value());
+		_pd->unbind_thread(this);
+	}
 
 	platform_thread_registry().remove(*this);
 	platform_specific()->core_sel_alloc().free(_pager_obj_sel);