diff --git a/spec/abstract/ARM_HYP/Hypervisor_A.thy b/spec/abstract/ARM_HYP/Hypervisor_A.thy
index 082359aa0..f8207f278 100644
--- a/spec/abstract/ARM_HYP/Hypervisor_A.thy
+++ b/spec/abstract/ARM_HYP/Hypervisor_A.thy
@@ -16,10 +16,10 @@ begin
 
 context Arch begin global_naming ARM_A
 
-fun handle_hypervisor_fault :: "word32 \<Rightarrow> hyp_fault_type \<Rightarrow> (unit, 'z::state_ext) f_monad"
+fun handle_hypervisor_fault :: "word32 \<Rightarrow> hyp_fault_type \<Rightarrow> (unit, 'z::state_ext) s_monad"
 where
 "handle_hypervisor_fault thread (ARMVCPUFault hsr) =
-   liftE (handle_fault thread (ArchFault $ VCPUFault hsr))"
+   handle_fault thread (ArchFault $ VCPUFault hsr)"
 
 
 end