diff --git a/headers/private/kernel/boot/kernel_args.h b/headers/private/kernel/boot/kernel_args.h
index 98f61b28d4..d5f41ceda6 100644
--- a/headers/private/kernel/boot/kernel_args.h
+++ b/headers/private/kernel/boot/kernel_args.h
@@ -7,7 +7,6 @@
 
 
 #include <SupportDefs.h>
-#include <platform_kernel_args.h>
 
 
 typedef struct address_range {
@@ -15,6 +14,9 @@ typedef struct address_range {
 	uint32 size;
 } addr_range;
 
+#include <platform_kernel_args.h>
+#include <arch_kernel_args.h>
+
 typedef struct kernel_args {
 	uint32		cons_line;
 	char		*str;
@@ -34,6 +36,7 @@ typedef struct kernel_args {
 	addr_range	cpu_kstack[MAX_BOOT_CPUS];
 
 	platform_kernel_args platform_args;
+	arch_kernel_args arch_args;
 
 	struct framebuffer {
 		int		enabled;