From 04fae5af329bd4f6ab0cdc4b11b8309da57f90ae Mon Sep 17 00:00:00 2001
From: Gerwin Klein <gerwin.klein@data61.csiro.au>
Date: Sat, 1 Apr 2017 10:29:58 +0200
Subject: [PATCH] arm-hyp abstract: hypervisor fault not itself allowed to
 fault

---
 spec/abstract/ARM_HYP/Hypervisor_A.thy | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

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