diff --git a/xen/arch/arm/include/asm/event.h b/xen/arch/arm/include/asm/event.h
index 509157b2b3..e036ab7fb8 100644
--- a/xen/arch/arm/include/asm/event.h
+++ b/xen/arch/arm/include/asm/event.h
@@ -3,7 +3,6 @@
 
 #include <asm/domain.h>
 
-void vcpu_kick(struct vcpu *v);
 void vcpu_mark_events_pending(struct vcpu *v);
 void vcpu_update_evtchn_irq(struct vcpu *v);
 void vcpu_block_unless_event_pending(struct vcpu *v);
diff --git a/xen/arch/ppc/include/asm/event.h b/xen/arch/ppc/include/asm/event.h
index 0f475c4b89..565eee1439 100644
--- a/xen/arch/ppc/include/asm/event.h
+++ b/xen/arch/ppc/include/asm/event.h
@@ -5,7 +5,6 @@
 #include <xen/lib.h>
 
 /* TODO: implement */
-static inline void vcpu_kick(struct vcpu *v) { BUG_ON("unimplemented"); }
 static inline void vcpu_mark_events_pending(struct vcpu *v) { BUG_ON("unimplemented"); }
 static inline void vcpu_update_evtchn_irq(struct vcpu *v) { BUG_ON("unimplemented"); }
 static inline void vcpu_block_unless_event_pending(struct vcpu *v) { BUG_ON("unimplemented"); }
diff --git a/xen/arch/x86/include/asm/event.h b/xen/arch/x86/include/asm/event.h
index 434f65007e..d13ce28167 100644
--- a/xen/arch/x86/include/asm/event.h
+++ b/xen/arch/x86/include/asm/event.h
@@ -11,7 +11,6 @@
 
 #include <xen/shared.h>
 
-void vcpu_kick(struct vcpu *v);
 void vcpu_mark_events_pending(struct vcpu *v);
 
 static inline int vcpu_event_delivery_is_enabled(struct vcpu *v)
diff --git a/xen/include/xen/sched.h b/xen/include/xen/sched.h
index 52090b4f70..1f77e0869b 100644
--- a/xen/include/xen/sched.h
+++ b/xen/include/xen/sched.h
@@ -877,6 +877,7 @@ void vcpu_wake(struct vcpu *v);
 long vcpu_yield(void);
 void vcpu_sleep_nosync(struct vcpu *v);
 void vcpu_sleep_sync(struct vcpu *v);
+void vcpu_kick(struct vcpu *v);
 
 /*
  * Force synchronisation of given VCPU's state. If it is currently descheduled,