diff --git a/include/arch/ia32/arch/api/objecttype.h b/include/arch/ia32/arch/api/objecttype.h
index 64fac5cca..a6f10e79a 100644
--- a/include/arch/ia32/arch/api/objecttype.h
+++ b/include/arch/ia32/arch/api/objecttype.h
@@ -11,6 +11,10 @@
 #ifndef __ARCH_OBJECT_TYPE_H
 #define __ARCH_OBJECT_TYPE_H
 
+#ifdef HAVE_AUTOCONF
+#include <autoconf.h>
+#endif /* HAVE_AUTOCONF */
+
 typedef enum _object {
     seL4_IA32_4K = seL4_NonArchObjectTypeCount,
     seL4_IA32_LargePage,
@@ -24,4 +28,10 @@ typedef enum _object {
 } seL4_ArchObjectType;
 typedef uint32_t object_t;
 
+/* Previously frame types were explcitly 4K and 4M. If not PAE
+ * we assume legacy environment and emulate old definitions */
+#ifndef CONFIG_PAE_PAGING
+#define seL4_IA32_4M seL4_IA32_LargePage
+#endif
+
 #endif
diff --git a/libsel4/arch_include/ia32/sel4/arch/objecttype.h b/libsel4/arch_include/ia32/sel4/arch/objecttype.h
index 38c551b40..107fb9141 100644
--- a/libsel4/arch_include/ia32/sel4/arch/objecttype.h
+++ b/libsel4/arch_include/ia32/sel4/arch/objecttype.h
@@ -11,7 +11,9 @@
 #ifndef __ARCH_OBJECT_TYPE_H
 #define __ARCH_OBJECT_TYPE_H
 
+#ifdef HAVE_AUTOCONF
 #include <autoconf.h>
+#endif /* HAVE_AUTOCONF */
 
 typedef enum _object {
     seL4_IA32_4K = seL4_NonArchObjectTypeCount,