diff --git a/spec/abstract/ARM_HYP/ArchVSpaceAcc_A.thy b/spec/abstract/ARM_HYP/ArchVSpaceAcc_A.thy
index 13dee4809..981534d34 100644
--- a/spec/abstract/ARM_HYP/ArchVSpaceAcc_A.thy
+++ b/spec/abstract/ARM_HYP/ArchVSpaceAcc_A.thy
@@ -88,6 +88,11 @@ definition
      set_object ptr (ArchObj (PageDirectory pd))
    od"
 
+definition
+  set_current_pd :: "paddr \<Rightarrow> unit machine_monad"
+where
+  "set_current_pd pd \<equiv> setCurrentPDPL2 pd"
+
 text {* The following function takes a pointer to a PDE in kernel memory
   and returns the actual PDE. *}
 definition
diff --git a/spec/abstract/ARM_HYP/ArchVSpace_A.thy b/spec/abstract/ARM_HYP/ArchVSpace_A.thy
index 594dca25c..2b1a4e37c 100644
--- a/spec/abstract/ARM_HYP/ArchVSpace_A.thy
+++ b/spec/abstract/ARM_HYP/ArchVSpace_A.thy
@@ -588,7 +588,7 @@ definition
      | _ \<Rightarrow> throwError InvalidRoot) <catch>
     (\<lambda>_. do
        global_us_pd \<leftarrow> gets (arm_us_global_pd o arch_state);
-       do_machine_op $ setCurrentPD $ addrFromPPtr global_us_pd
+       do_machine_op $ set_current_pd $ addrFromPPtr global_us_pd
     od)
 od"
 
diff --git a/spec/machine/ARM_HYP/MachineOps.thy b/spec/machine/ARM_HYP/MachineOps.thy
index 92e6cc016..2bc8e1e54 100644
--- a/spec/machine/ARM_HYP/MachineOps.thy
+++ b/spec/machine/ARM_HYP/MachineOps.thy
@@ -157,14 +157,11 @@ definition
   dmb :: "unit machine_monad"
 where "dmb \<equiv> machine_op_lift dmb_impl"
 
-
+consts'
+  setCurrentPDPL2_impl :: "paddr \<Rightarrow> unit machine_rest_monad"
 definition
-  setCurrentPD :: "paddr \<Rightarrow> unit machine_monad"
-where "setCurrentPD pd \<equiv> do
-             dsb;
-             writeTTBR0 pd;
-             isb
-          od"
+  setCurrentPDPL2 :: "paddr \<Rightarrow> unit machine_monad"
+where "setCurrentPDPL2 pd \<equiv> machine_op_lift (setCurrentPDPL2_impl pd)"
 
 consts'
   invalidateTLB_impl :: "unit machine_rest_monad"