diff --git a/libsel4allocman/include/allocman/bootstrap.h b/libsel4allocman/include/allocman/bootstrap.h
index 30f95b0..9c0dcba 100644
--- a/libsel4allocman/include/allocman/bootstrap.h
+++ b/libsel4allocman/include/allocman/bootstrap.h
@@ -57,7 +57,6 @@
 #include <allocman/mspace/fixed_pool.h>
 #include <allocman/mspace/virtual_pool.h>
 #include <allocman/utspace/twinkle.h>
-#include <allocman/utspace/trickle.h>
 #include <vspace/vspace.h>
 #include <simple/simple.h>
 /**
diff --git a/libsel4allocman/include/allocman/utspace/trickle.h b/libsel4allocman/include/allocman/utspace/trickle.h
deleted file mode 100644
index 8fa6dda..0000000
--- a/libsel4allocman/include/allocman/utspace/trickle.h
+++ /dev/null
@@ -1,61 +0,0 @@
-/*
- * Copyright 2014, NICTA
- *
- * This software may be distributed and modified according to the terms of
- * the BSD 2-Clause license. Note that NO WARRANTY is provided.
- * See "LICENSE_BSD2.txt" for details.
- *
- * @TAG(NICTA_BSD)
- */
-
-#ifndef _ALLOCMAN_UTSPACE_TRICKLE_H_
-#define _ALLOCMAN_UTSPACE_TRICKLE_H_
-
-#include <autoconf.h>
-#include <sel4/types.h>
-#include <allocman/utspace/utspace.h>
-#include <assert.h>
-
-#ifdef CONFIG_KERNEL_STABLE
-
-struct utspace_trickle_node {
-    cspacepath_t *ut;
-    size_t offset;
-    seL4_Word parent_cookie;
-    size_t bitmap_bits;
-    size_t bitmap;
-    struct utspace_trickle_node *next, *prev;
-    size_t padding;
-    uintptr_t paddr;
-};
-
-compile_time_assert(trickle_struct_size32, sizeof(struct utspace_trickle_node) == 36 || sizeof(size_t) == 8);
-compile_time_assert(trickle_struct_size64, sizeof(struct utspace_trickle_node) == 72 || sizeof(size_t) == 4);
-
-typedef struct utspace_trickle {
-    struct utspace_trickle_node *heads[CONFIG_WORD_SIZE];
-} utspace_trickle_t;
-
-void utspace_trickle_create(utspace_trickle_t *trickle);
-
-int _utspace_trickle_add_uts(struct allocman *alloc, void *_trickle, size_t num, const cspacepath_t *uts, size_t *size_bits, uintptr_t *paddr);
-
-seL4_Word _utspace_trickle_alloc(struct allocman *alloc, void *_trickle, size_t size_bits, seL4_Word type, const cspacepath_t *slot, int *error);
-void _utspace_trickle_free(struct allocman *alloc, void *_trickle, seL4_Word cookie, size_t size_bits);
-
-uintptr_t _utspace_trickle_paddr(void *_trickle, seL4_Word cookie, size_t size_bits);
-
-static inline utspace_interface_t utspace_trickle_make_interface(utspace_trickle_t *trickle) {
-    return (utspace_interface_t) {
-        .alloc = _utspace_trickle_alloc,
-        .free = _utspace_trickle_free,
-        .add_uts = _utspace_trickle_add_uts,
-        .paddr = _utspace_trickle_paddr,
-        .properties = ALLOCMAN_DEFAULT_PROPERTIES,
-        .utspace = trickle
-    };
-}
-
-#endif /* CONFIG_KERNEL_STABLE */
-
-#endif
diff --git a/libsel4allocman/src/bootstrap.c b/libsel4allocman/src/bootstrap.c
index 9f06f08..9debfa2 100644
--- a/libsel4allocman/src/bootstrap.c
+++ b/libsel4allocman/src/bootstrap.c
@@ -15,7 +15,6 @@
 #include <allocman/cspace/simple1level.h>
 #include <allocman/cspace/two_level.h>
 #include <allocman/mspace/dual_pool.h>
-#include <allocman/utspace/trickle.h>
 #include <allocman/utspace/split.h>
 #include <allocman/bootstrap.h>
 #include <allocman/sel4_arch/reservation.h>
@@ -28,11 +27,7 @@
 #include <utils/arith.h>
 
 /* configure the choice of boot strapping allocators */
-#if defined(CONFIG_KERNEL_STABLE)
-#define UTMAN trickle
-#else
 #define UTMAN split
-#endif
 
 /*do some nasty macro expansion to get the string substitution to happen how we want */
 #define CON2(a, b,c) a##b##c
@@ -275,37 +270,6 @@
     return 0;
 }
 
-#if defined(CONFIG_KERNEL_STABLE)
-
-static int _split_ut(bootstrap_info_t *bs, cspacepath_t ut, cspacepath_t p1, cspacepath_t p2, size_t size) {
-    int error;
-    error = seL4_Untyped_RetypeAtOffset(ut.capPtr, seL4_UntypedObject, 0, size, p1.root, p1.dest, p1.destDepth, p1.offset, 1);
-    if (error != seL4_NoError) {
-        LOG_ERROR("Failed to split untyped");
-        return 1;
-    }
-    error = seL4_Untyped_RetypeAtOffset(ut.capPtr, seL4_UntypedObject, BIT(size), size,
-                                        p2.root, p2.dest, p2.destDepth, p2.offset, 1);
-    if (error != seL4_NoError) {
-        LOG_ERROR("Failed to allocate second half of split untyped");
-        return 1;
-    }
-    return 0;
-}
-
-static int _retype_cnode(bootstrap_info_t *bs, cspacepath_t ut, cspacepath_t cnode, seL4_Word sel4_size) {
-    int error;
-    error = seL4_Untyped_RetypeAtOffset(ut.capPtr, seL4_CapTableObject, 0, sel4_size,
-                                        cnode.root, cnode.dest, cnode.destDepth, cnode.offset, 1);
-    if (error != seL4_NoError) {
-        LOG_ERROR("Failed to retype a cnode");
-        return 1;
-    }
-    return 0;
-}
-
-#else
-
 static int _split_ut(bootstrap_info_t *bs, cspacepath_t ut, cspacepath_t p1, cspacepath_t p2, size_t size) {
     int error;
     error = seL4_Untyped_Retype(ut.capPtr, seL4_UntypedObject, size, p1.root, p1.dest, p1.destDepth, p1.offset, 1);
@@ -329,8 +293,6 @@
     return 0;
 }
 
-#endif
-
 static int bootstrap_allocate_cnode(bootstrap_info_t *bs, size_t size, cspacepath_t *slot) {
     size_t ut_size;
     int i;
diff --git a/libsel4allocman/src/utspace/split.c b/libsel4allocman/src/utspace/split.c
index 416348c..b255d8d 100644
--- a/libsel4allocman/src/utspace/split.c
+++ b/libsel4allocman/src/utspace/split.c
@@ -135,11 +135,7 @@
         return 1;
     }
     /* perform the first retype */
-#if defined(CONFIG_KERNEL_STABLE)
-    sel4_error = seL4_Untyped_RetypeAtOffset(node->ut.capPtr, seL4_UntypedObject, 0, size_bits, left->ut.root, left->ut.dest, left->ut.destDepth, left->ut.offset, 1);
-#else
     sel4_error = seL4_Untyped_Retype(node->ut.capPtr, seL4_UntypedObject, size_bits, left->ut.root, left->ut.dest, left->ut.destDepth, left->ut.offset, 1);
-#endif
     if (sel4_error != seL4_NoError) {
         _delete_node(alloc, left);
         _delete_node(alloc, right);
@@ -147,11 +143,7 @@
         return 1;
     }
     /* perform the second retype */
-#if defined(CONFIG_KERNEL_STABLE)
-    sel4_error = seL4_Untyped_RetypeAtOffset(node->ut.capPtr, seL4_UntypedObject, BIT(size_bits), size_bits, right->ut.root, right->ut.dest, right->ut.destDepth, right->ut.offset, 1);
-#else
     sel4_error = seL4_Untyped_Retype(node->ut.capPtr, seL4_UntypedObject, size_bits, right->ut.root, right->ut.dest, right->ut.destDepth, right->ut.offset, 1);
-#endif
     if (sel4_error != seL4_NoError) {
         vka_cnode_delete(&left->ut);
         _delete_node(alloc, left);
@@ -199,11 +191,7 @@
     /* use the first node for lack of a better one */
     node = split->heads[size_bits];
     /* Perform the untyped retype */
-#if defined(CONFIG_KERNEL_STABLE)
-    sel4_error = seL4_Untyped_RetypeAtOffset(node->ut.capPtr, type, 0, sel4_size_bits, slot->root, slot->dest, slot->destDepth, slot->offset, 1);
-#else
     sel4_error = seL4_Untyped_Retype(node->ut.capPtr, type, sel4_size_bits, slot->root, slot->dest, slot->destDepth, slot->offset, 1);
-#endif
     if (sel4_error != seL4_NoError) {
         /* Well this shouldn't happen */
         SET_ERROR(error, 1);
diff --git a/libsel4allocman/src/utspace/trickle.c b/libsel4allocman/src/utspace/trickle.c
deleted file mode 100644
index 80e039e..0000000
--- a/libsel4allocman/src/utspace/trickle.c
+++ /dev/null
@@ -1,251 +0,0 @@
-/*
- * Copyright 2014, NICTA
- *
- * This software may be distributed and modified according to the terms of
- * the BSD 2-Clause license. Note that NO WARRANTY is provided.
- * See "LICENSE_BSD2.txt" for details.
- *
- * @TAG(NICTA_BSD)
- */
-
-#include <autoconf.h>
-#include <allocman/utspace/trickle.h>
-#include <allocman/allocman.h>
-#include <allocman/util.h>
-#include <sel4/sel4.h>
-
-#include <vka/object.h>
-
-#ifdef CONFIG_KERNEL_STABLE
-
-static inline size_t _make_bitmap(size_t bits) {
-    /* avoid shift by int max in BIT/MASK code */
-    if (BIT(bits - 1) == CONFIG_WORD_SIZE) {
-        return -1;
-    } else {
-        /* shift the result up so that the high bits are set */
-        return MASK(BIT(bits - 1)) << (CONFIG_WORD_SIZE - BIT(bits - 1));
-    }
-}
-
-static inline void _insert_node(struct utspace_trickle_node **head, struct utspace_trickle_node *node)
-{
-    if (*head) {
-        (*head)->prev = node;
-    }
-    node->next = *head;
-    node->prev = NULL;
-    *head = node;
-}
-
-static inline void _remove_node(struct utspace_trickle_node **head, struct utspace_trickle_node *node)
-{
-    if (node->next) {
-        node->next->prev = node->prev;
-    }
-    if (node->prev) {
-        node->prev->next = node->next;
-    } else {
-        *head = node->next;
-    }
-}
-
-static inline seL4_Word _make_cookie(struct utspace_trickle_node *node, size_t offset)
-{
-    size_t int_node = (size_t) node;
-    assert( (int_node % (CONFIG_WORD_SIZE)) == 0);
-    assert(offset < CONFIG_WORD_SIZE);
-    return int_node | offset;
-}
-
-static inline struct utspace_trickle_node *_cookie_to_node(seL4_Word cookie) {
-    cookie -= cookie % (CONFIG_WORD_SIZE);
-    return (struct utspace_trickle_node*)cookie;
-}
-
-static inline size_t _cookie_to_offset(seL4_Word cookie)
-{
-    return cookie % (CONFIG_WORD_SIZE);
-}
-
-static inline struct utspace_trickle_node *_make_node(struct allocman *alloc, int *error) {
-    uintptr_t addr = (uintptr_t)allocman_mspace_alloc(alloc, sizeof(struct utspace_trickle_node) * 2 - sizeof(size_t), error);
-    struct utspace_trickle_node *node;
-    if (*error) {
-        return NULL;
-    }
-    node = _cookie_to_node(addr + CONFIG_WORD_SIZE);
-    node->padding = addr;
-    return node;
-}
-
-static inline void _free_node(struct allocman *alloc, struct utspace_trickle_node *node)
-{
-    allocman_mspace_free(alloc, (void*)node->padding, sizeof(struct utspace_trickle_node) * 2 - sizeof(size_t));
-}
-
-int _utspace_trickle_add_uts(allocman_t *alloc, void *_trickle, size_t num, const cspacepath_t *uts, size_t *size_bits, uintptr_t *paddr) {
-    utspace_trickle_t *trickle = (utspace_trickle_t*) _trickle;
-    struct utspace_trickle_node *nodes[num];
-    cspacepath_t *uts_copy[num];
-    int error;
-    size_t i;
-    for (i = 0; i < num; i++) {
-        nodes[i] = _make_node(alloc, &error);
-        if (error) {
-            for (i--; i >= 0; i--) {
-                _free_node(alloc, nodes[i]);
-                allocman_mspace_free(alloc, uts_copy[i], sizeof(cspacepath_t));
-            }
-            return error;
-        }
-        uts_copy[i] = allocman_mspace_alloc(alloc, sizeof(cspacepath_t), &error);
-        if (error) {
-            _free_node(alloc, nodes[i]);
-            for (i--; i >= 0; i--) {
-                _free_node(alloc, nodes[i]);
-                allocman_mspace_free(alloc, uts_copy[i], sizeof(cspacepath_t));
-            }
-        }
-    }
-    for (i = 0; i < num; i++) {
-        *uts_copy[i] = uts[i];
-        nodes[i]->ut = uts_copy[i];
-        nodes[i]->offset = 0;
-        nodes[i]->paddr = paddr[i];
-        nodes[i]->parent_cookie = 0;
-        nodes[i]->next = nodes[i]->prev = NULL;
-        /* Start with only 1 thing free */
-        nodes[i]->bitmap = BIT(31);
-        nodes[i]->bitmap_bits = 1;
-        _insert_node(&trickle->heads[size_bits[i]], nodes[i]);
-    }
-    return 0;
-}
-
-void utspace_trickle_create(utspace_trickle_t *trickle)
-{
-    uint32_t i;
-    for (i = 0; i < CONFIG_WORD_SIZE; i++) {
-        trickle->heads[i] = NULL;
-    }
-}
-
-static int _refill_pool(struct allocman *alloc, utspace_trickle_t *trickle, size_t size_bits)
-{
-    size_t i;
-    int error;
-    struct utspace_trickle_node *node;
-    seL4_Word cookie;
-    node = _make_node(alloc, &error);
-    if (error) {
-        return error;
-    }
-    /* Check if there are untypeds >= 5 size_bits from us */
-    for (i = size_bits + 5 > CONFIG_WORD_SIZE - 1 ? CONFIG_WORD_SIZE - 1 : size_bits + 5; i < CONFIG_WORD_SIZE; i++) {
-        if (trickle->heads[i]) {
-            i = size_bits + 5;
-            break;
-        }
-    }
-    if (i == CONFIG_WORD_SIZE) {
-        /* Search for the biggest one near us */
-        for (i = size_bits + 5 > CONFIG_WORD_SIZE - 1 ? CONFIG_WORD_SIZE - 1 : size_bits + 5; i > size_bits; i--) {
-            if (trickle->heads[i]) {
-                break;
-            }
-        }
-    }
-    if (i != size_bits) {
-        cookie = _utspace_trickle_alloc(alloc, trickle, i, seL4_UntypedObject, NULL, &error);
-        if (!error) {
-            struct utspace_trickle_node *parent = _cookie_to_node(cookie);
-            size_t offset = _cookie_to_offset(cookie);
-            node->ut = parent->ut;
-            node->offset = parent->offset + (offset << (i));
-            if (parent->paddr) {
-                node->paddr = parent->paddr + (offset << (i));
-            } else {
-                node->paddr = 0;
-            }
-            node->parent_cookie = cookie;
-            node->bitmap_bits = i - size_bits + 1;
-            node->bitmap = _make_bitmap(node->bitmap_bits);
-            node->next = node->prev = NULL;
-            _insert_node(&trickle->heads[size_bits], node);
-            return 0;
-        }
-    }
-    _free_node(alloc, node);
-    return 1;
-}
-
-seL4_Word _utspace_trickle_alloc(struct allocman *alloc, void *_trickle, size_t size_bits, seL4_Word type, const cspacepath_t *slot, int *error)
-{
-    size_t sel4_size_bits;
-    int _error;
-    utspace_trickle_t *trickle = (utspace_trickle_t*)_trickle;
-    struct utspace_trickle_node *node;
-    size_t offset;
-    size_t mem_offset;
-    /* get size of untyped call */
-    sel4_size_bits = get_sel4_object_size(type, size_bits);
-    if (size_bits != vka_get_object_size(type, sel4_size_bits) || size_bits == 0) {
-        SET_ERROR(error, 1);
-        return 0;
-    }
-    assert(size_bits < CONFIG_WORD_SIZE);
-    if (!trickle->heads[size_bits]) {
-        _error = _refill_pool(alloc, trickle, size_bits);
-        if (_error) {
-            SET_ERROR(error, _error);
-            return 0;
-        }
-    }
-    node = trickle->heads[size_bits];
-    offset = CLZL(node->bitmap);
-    mem_offset = node->offset + (offset << size_bits);
-    if (slot) {
-        _error = seL4_Untyped_RetypeAtOffset(node->ut->capPtr, type, mem_offset, sel4_size_bits, slot->root, slot->dest, slot->destDepth, slot->offset, 1);
-        if (_error != seL4_NoError) {
-            SET_ERROR(error, 1);
-            return 0;
-        }
-    }
-    node->bitmap &= ~BIT(CONFIG_WORD_SIZE - 1 - offset);
-    if (node->bitmap == 0) {
-        _remove_node(&trickle->heads[size_bits], node);
-    }
-    SET_ERROR(error, 0);
-    return _make_cookie(node, offset);
-}
-
-void _utspace_trickle_free(struct allocman *alloc, void *_trickle, seL4_Word cookie, size_t size_bits)
-{
-    utspace_trickle_t *trickle = (utspace_trickle_t*)_trickle;
-    struct utspace_trickle_node *node = _cookie_to_node(cookie);
-    size_t offset = _cookie_to_offset(cookie);
-    int in_list = !(node->bitmap == 0);
-    node->bitmap |= BIT(CONFIG_WORD_SIZE - 1 - offset);
-    if (node->bitmap == _make_bitmap(node->bitmap_bits)) {
-        if (node->parent_cookie) {
-            if (in_list) {
-                _remove_node(&trickle->heads[size_bits], node);
-            }
-            _utspace_trickle_free(alloc, trickle, node->parent_cookie, size_bits + node->bitmap_bits - 1);
-            _free_node(alloc, node);
-        } else if (!in_list) {
-            _insert_node(&trickle->heads[size_bits], node);
-        }
-    } else if (!in_list) {
-        _insert_node(&trickle->heads[size_bits], node);
-    }
-}
-
-uintptr_t _utspace_trickle_paddr(void *_trickle, seL4_Word cookie, size_t size_bits) {
-    struct utspace_trickle_node *node = _cookie_to_node(cookie);
-    size_t offset = _cookie_to_offset(cookie);
-    return node->paddr + (offset << size_bits);
-}
-
-#endif
diff --git a/libsel4allocman/src/utspace/twinkle.c b/libsel4allocman/src/utspace/twinkle.c
index 908e763..7e3681f 100644
--- a/libsel4allocman/src/utspace/twinkle.c
+++ b/libsel4allocman/src/utspace/twinkle.c
@@ -82,15 +82,10 @@
             i = j;
         }
     }
-    /* Perform the untyped retype */
-#if defined(CONFIG_KERNEL_STABLE)
-    sel4_error = seL4_Untyped_RetypeAtOffset(twinkle->uts[i].path.capPtr, type, _round_up(twinkle->uts[i].offset, size_bits), sel4_size_bits, slot->root, slot->dest, slot->destDepth, slot->offset, 1);
-#else
     /* if using inc retype then our offset calculation is effectively emulating the kernels calculations. This
      * means we track the free space of the untyped correctly, and since we are not going to try and free then
      * allocate again, this allocator can be used with either allocation scheme */
     sel4_error = seL4_Untyped_Retype(twinkle->uts[i].path.capPtr, type, sel4_size_bits, slot->root, slot->dest, slot->destDepth, slot->offset, 1);
-#endif
     if (sel4_error != seL4_NoError) {
         /* Well this shouldn't happen */
         SET_ERROR(error, 1);
diff --git a/libsel4debug/src/bootinfo.c b/libsel4debug/src/bootinfo.c
index a0f9616..ec55b9b 100644
--- a/libsel4debug/src/bootinfo.c
+++ b/libsel4debug/src/bootinfo.c
@@ -49,19 +49,6 @@
         }
     }
 
-    /* mainline and experimental treat device regions differently*/
-#ifdef CONFIG_KERNEL_STABLE
-    ZF_LOGI("device untypeds: [%u --> %u)", info->deviceUntyped.start, info->deviceUntyped.end);
-    ZF_LOGI("List of device untypes");
-    ZF_LOGI("Paddr    | Size   ");
-    int start = info->untyped.end - info->untyped.start;
-    int size = info->deviceUntyped.end - info->deviceUntyped.start;
-    for (int i = start; i < start + size; i++) {
-        if (info->untypedPaddrList[i] != 0) {
-            ZF_LOGI("0x%08x | %u", info->untypedPaddrList[i], info->untypedSizeBitsList[i]);
-        }
-    }
-#else
     ZF_LOGI("DeviceRegions: %u\n", info->numDeviceRegions);
     printf("List of deviceRegions\n");
     printf("Paddr    | Size     | Slot Region\n");
@@ -71,7 +58,6 @@
                info->deviceRegions[i].frames.start,
                info->deviceRegions[i].frames.end);
     }
-#endif /* CONFIG_KERNEL_STABLE */
 
 }
 
diff --git a/libsel4utils/include/sel4utils/process.h b/libsel4utils/include/sel4utils/process.h
index 1186dbf..ddbe650 100644
--- a/libsel4utils/include/sel4utils/process.h
+++ b/libsel4utils/include/sel4utils/process.h
@@ -118,9 +118,7 @@
     vka_object_t fault_endpoint;
 
     int priority;
-#ifndef CONFIG_KERNEL_STABLE
     seL4_CPtr asid_pool;
-#endif
 } sel4utils_process_config_t;
 
 /**
diff --git a/libsel4utils/src/page_dma.c b/libsel4utils/src/page_dma.c
index 0ece05e..75193f2 100644
--- a/libsel4utils/src/page_dma.c
+++ b/libsel4utils/src/page_dma.c
@@ -112,11 +112,7 @@
         if (error) {
             goto handle_error;
         }
-#ifdef CONFIG_KERNEL_STABLE
-        error = seL4_Untyped_RetypeAtOffset(ut.cptr, kobject_get_type(KOBJECT_FRAME, PAGE_BITS_4K), PAGE_SIZE_4K * i, size_bits, frames[i].root, frames[i].dest, frames[i].destDepth, frames[i].offset, 1);
-#else
         error = seL4_Untyped_Retype(ut.cptr, kobject_get_type(KOBJECT_FRAME, PAGE_BITS_4K), size_bits, frames[i].root, frames[i].dest, frames[i].destDepth, frames[i].offset, 1);
-#endif
         if (error != seL4_NoError) {
             goto handle_error;
         }
diff --git a/libsel4utils/src/process.c b/libsel4utils/src/process.c
index e166d9b..fe3b992 100644
--- a/libsel4utils/src/process.c
+++ b/libsel4utils/src/process.c
@@ -369,9 +369,7 @@
         .create_vspace = true,
         .create_fault_endpoint = true,
         .priority = priority,
-#ifndef CONFIG_KERNEL_STABLE
         .asid_pool = seL4_CapInitThreadASIDPool,
-#endif
     };
 
     return sel4utils_configure_process_custom(process, vka, vspace, config);
@@ -459,7 +457,7 @@
     slot = sel4utils_copy_cap_to_process(process, src);
     assert(slot == SEL4UTILS_PD_SLOT);
 
-    if (!(config_set(CONFIG_KERNEL_STABLE) || config_set(CONFIG_X86_64))) {
+    if (!config_set(CONFIG_X86_64)) {
         vka_cspace_make_path(vka, get_asid_pool(asid_pool), &src);
         slot = sel4utils_copy_cap_to_process(process, src);
         assert(slot == SEL4UTILS_ASID_POOL_SLOT);
@@ -501,7 +499,7 @@
         }
 
         /* assign an asid pool */
-        if (!(config_set(CONFIG_KERNEL_STABLE) || config_set(CONFIG_X86_64)) &&
+        if (!config_set(CONFIG_X86_64) &&
               assign_asid_pool(config.asid_pool, process->pd.cptr) != seL4_NoError) {
             goto error;
         }
diff --git a/libsel4utils/src/vspace/bootstrap.c b/libsel4utils/src/vspace/bootstrap.c
index 95ae31f..868e934 100644
--- a/libsel4utils/src/vspace/bootstrap.c
+++ b/libsel4utils/src/vspace/bootstrap.c
@@ -19,10 +19,6 @@
 #include <sel4utils/vspace.h>
 #include <sel4utils/vspace_internal.h>
 
-#ifdef CONFIG_KERNEL_STABLE
-#include <sel4/arch/bootinfo.h>
-#endif
-
 /* For the initial vspace, we must always guarantee we have virtual memory available
  * for each bottom level page table. Future vspaces can then use the initial vspace
  * to allocate bottom level page tables until memory runs out.
@@ -373,9 +369,6 @@
 {
     void *existing_frames[] = {
         (void *) info,
-#if defined(CONFIG_ARCH_X86) && defined(CONFIG_KERNEL_STABLE)
-        (void *) seL4_IA32_GetBootInfo(),
-#endif
         /* We assume the IPC buffer is less than a page and fits into one page */
         (void *) (seL4_Word)ROUND_DOWN(((seL4_Word)(info->ipcBuffer)), PAGE_SIZE_4K),
         NULL
diff --git a/libsel4vka/include/vka/capops.h b/libsel4vka/include/vka/capops.h
index 98b377b..736c0f0 100644
--- a/libsel4vka/include/vka/capops.h
+++ b/libsel4vka/include/vka/capops.h
@@ -131,17 +131,6 @@
 //TODO: implement rotate
 
 
-#ifdef CONFIG_KERNEL_STABLE
-inline static int
-vka_untyped_retypeAtOffset(vka_object_t *untyped, int type, int offset, int size_bits,
-                           int num_objects, const cspacepath_t *dest)
-{
-    size_bits = vka_get_object_size(type, size_bits);
-    return seL4_Untyped_RetypeAtOffset(untyped->cptr, type, offset, size_bits,
-                                       dest->root, dest->dest, dest->destDepth, dest->offset, num_objects);
-}
-
-#else
 /**
  * Retype num_objects objects from untyped into type starting from destination slot dest.
  *
@@ -153,6 +142,5 @@
     size_bits = vka_get_object_size(type, size_bits);
     return seL4_Untyped_Retype(untyped->cptr, type, size_bits, dest->root, dest->dest, dest->destDepth, dest->offset, num_objects);
 }
-#endif
 
 #endif /* VKA_CAPOPS_H */