Index: kernel/arch/ppc32/src/interrupt.c
===================================================================
--- kernel/arch/ppc32/src/interrupt.c	(revision fc468841de2b95bece0894c87ba698651aa540fe)
+++ kernel/arch/ppc32/src/interrupt.c	(revision d95f1e24a3ed2800461f743a8f9c97803cacd0a1)
@@ -81,17 +81,4 @@
 }
 
-
-static void ipc_int(int n, istate_t *istate)
-{
-	ipc_irq_send_notif(n - INT_OFFSET);
-}
-
-
-/* Reregister irq to be IPC-ready */
-void irq_ipc_bind_arch(unative_t irq)
-{
-	int_register(irq, "ipc_int", ipc_int);
-}
-
 /** @}
  */
Index: kernel/generic/src/ddi/device.c
===================================================================
--- kernel/generic/src/ddi/device.c	(revision fc468841de2b95bece0894c87ba698651aa540fe)
+++ kernel/generic/src/ddi/device.c	(revision d95f1e24a3ed2800461f743a8f9c97803cacd0a1)
@@ -35,4 +35,5 @@
  */
 
+#include <arch/types.h>
 #include <ddi/device.h>
 #include <atomic.h>