diff --git a/xen/arch/x86/domain.c b/xen/arch/x86/domain.c
index 66b7412b87..3a21e035f4 100644
--- a/xen/arch/x86/domain.c
+++ b/xen/arch/x86/domain.c
@@ -571,15 +571,20 @@ int arch_vcpu_create(struct vcpu *v)
 
     if ( is_hvm_domain(d) )
         rc = hvm_vcpu_initialise(v);
-    else if ( !is_idle_domain(d) )
-        rc = pv_vcpu_initialise(v);
-    else
+    else if ( is_idle_domain(d) )
     {
         /* Idle domain */
         v->arch.cr3 = __pa(idle_pg_table);
         rc = 0;
         v->arch.msrs = ZERO_BLOCK_PTR; /* Catch stray misuses */
     }
+    else if ( IS_ENABLED(CONFIG_PV) )
+        rc = pv_vcpu_initialise(v);
+    else
+    {
+        ASSERT_UNREACHABLE();
+        rc = -EOPNOTSUPP;
+    }
 
     if ( rc )
         goto fail;
@@ -614,8 +619,10 @@ void arch_vcpu_destroy(struct vcpu *v)
 
     if ( is_hvm_vcpu(v) )
         hvm_vcpu_destroy(v);
-    else
+    else if ( IS_ENABLED(CONFIG_PV) )
         pv_vcpu_destroy(v);
+    else
+        ASSERT_UNREACHABLE();
 }
 
 int arch_sanitise_domain_config(struct xen_domctl_createdomain *config)
diff --git a/xen/arch/x86/include/asm/pv/domain.h b/xen/arch/x86/include/asm/pv/domain.h
index 75a6b9e5c7..582d004051 100644
--- a/xen/arch/x86/include/asm/pv/domain.h
+++ b/xen/arch/x86/include/asm/pv/domain.h
@@ -54,8 +54,6 @@ static inline unsigned long get_pcid_bits(const struct vcpu *v, bool is_xpti)
 #endif
 }
 
-#ifdef CONFIG_PV
-
 void pv_vcpu_destroy(struct vcpu *v);
 int pv_vcpu_initialise(struct vcpu *v);
 void pv_domain_destroy(struct domain *d);
@@ -84,29 +82,6 @@ void pv_set_reg(struct vcpu *v, unsigned int reg, uint64_t val);
 
 bool xpti_pcid_enabled(void);
 
-#else  /* !CONFIG_PV */
-
-#include <xen/errno.h>
-
-static inline void pv_vcpu_destroy(struct vcpu *v) {}
-static inline int pv_vcpu_initialise(struct vcpu *v) { return -EOPNOTSUPP; }
-static inline void pv_domain_destroy(struct domain *d) {}
-static inline int pv_domain_initialise(struct domain *d) { return -EOPNOTSUPP; }
-
-static inline unsigned long pv_make_cr4(const struct vcpu *v) { return ~0UL; }
-
-static inline uint64_t pv_get_reg(struct vcpu *v, unsigned int reg)
-{
-    ASSERT_UNREACHABLE();
-    return 0;
-}
-static inline void pv_set_reg(struct vcpu *v, unsigned int reg, uint64_t val)
-{
-    ASSERT_UNREACHABLE();
-}
-
-#endif	/* CONFIG_PV */
-
 void cf_check paravirt_ctxt_switch_from(struct vcpu *v);
 void cf_check paravirt_ctxt_switch_to(struct vcpu *v);