diff --git a/libsel4/sel4_arch_include/aarch32/sel4/sel4_arch/faults.h b/libsel4/sel4_arch_include/aarch32/sel4/sel4_arch/faults.h
index 1c81e5948..9d59a4bb4 100644
--- a/libsel4/sel4_arch_include/aarch32/sel4/sel4_arch/faults.h
+++ b/libsel4/sel4_arch_include/aarch32/sel4/sel4_arch/faults.h
@@ -47,9 +47,9 @@ seL4_getArchFault(seL4_MessageInfo_t tag)
                                       seL4_GetMR(seL4_VMFault_FSR));
 #ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
     case seL4_Fault_VGICMaintenance:
-        return seL4_Fault_VGICMaintenance_new(seL4_GetMR(seL4_Fault_VGICMaintenance_IDX));
+        return seL4_Fault_VGICMaintenance_new(seL4_GetMR(seL4_VGICMaintenance_IDX));
     case seL4_Fault_VCPUFault:
-        return seL4_Fault_VCPUFault_new(seL4_GetMR(seL4_Fault_VCPUFault_HSR));
+        return seL4_Fault_VCPUFault_new(seL4_GetMR(seL4_VCPUFault_HSR));
 #endif /* CONFIG_ARM_HYPERVISOR_SUPPORT */
     default:
         return seL4_Fault_NullFault_new();