diff --git a/spec/abstract/ARM_HYP/ArchDecode_A.thy b/spec/abstract/ARM_HYP/ArchDecode_A.thy
index af8d95e81..60ecfbc8c 100644
--- a/spec/abstract/ARM_HYP/ArchDecode_A.thy
+++ b/spec/abstract/ARM_HYP/ArchDecode_A.thy
@@ -147,15 +147,21 @@ case cap of
              attr = args ! 2;
              pd_cap = fst (extra_caps ! 0)
         in doE
-            whenE (mapped_address \<noteq> None) $ throwError $ InvalidCapability 0;
             (pd,asid) \<leftarrow> (case pd_cap of
                             ArchObjectCap (PageDirectoryCap pd (Some asid)) \<Rightarrow>
                               returnOk (pd,asid)
                          | _ \<Rightarrow> throwError $ InvalidCapability 1);
+            case mapped_address of
+              Some (asid', vaddr') \<Rightarrow> doE
+                whenE (asid' \<noteq> asid) (throwError $ InvalidCapability 1);
+                whenE (vaddr' \<noteq> vaddr) (throwError $ InvalidArgument 0)
+              odE
+            | None \<Rightarrow> doE
+                vtop \<leftarrow> returnOk (vaddr + (1 << (pageBitsForSize pgsz)) - 1);
+                whenE (vtop \<ge> kernel_base) $ throwError $ InvalidArgument 0
+              odE;
             pd' \<leftarrow> lookup_error_on_failure False $ find_pd_for_asid asid;
             whenE (pd' \<noteq> pd) $ throwError $ InvalidCapability 1;
-            vtop \<leftarrow> returnOk (vaddr + (1 << (pageBitsForSize pgsz)) - 1);
-            whenE (vtop \<ge> kernel_base) $ throwError $ InvalidArgument 0;
             vm_rights \<leftarrow> returnOk (mask_vm_rights R (data_to_rights rights_mask));
             check_vp_alignment pgsz vaddr;
             entries \<leftarrow> create_mapping_entries (addrFromPPtr p)
@@ -166,32 +172,7 @@ case cap of
                 (ArchObjectCap $ PageCap dev p R pgsz (Some (asid, vaddr)))
                 cte entries
         odE
-    else  throwError TruncatedMessage
-    else if invocation_type label = ArchInvocationLabel ARMPageRemap then
-         if length args > 1 \<and> length extra_caps > 0
-         then let rights_mask = args ! 0;
-                  attr = args ! 1;
-                  pd_cap = fst (extra_caps ! 0)
-         in doE
-            whenE (isIOSpaceFrame cap) $ throwError IllegalOperation;
-            (pd,asid) \<leftarrow> (case pd_cap of
-                            ArchObjectCap (PageDirectoryCap pd (Some asid)) \<Rightarrow>
-                              returnOk (pd,asid)
-                         | _ \<Rightarrow> throwError $ InvalidCapability 1);
-            (asid', vaddr) \<leftarrow> (case mapped_address of
-                  Some a \<Rightarrow> returnOk a
-                | _ \<Rightarrow> throwError $ InvalidCapability 0);
-            pd' \<leftarrow> lookup_error_on_failure False $ find_pd_for_asid asid';
-            whenE (pd' \<noteq> pd \<or> asid' \<noteq> asid) $ throwError $ InvalidCapability 1;
-            vm_rights \<leftarrow> returnOk (mask_vm_rights R $ data_to_rights rights_mask);
-            check_vp_alignment pgsz vaddr;
-            entries \<leftarrow> create_mapping_entries (addrFromPPtr p)
-                                              vaddr pgsz vm_rights
-                                              (attribs_from_word attr) pd;
-            ensure_safe_mapping entries;
-            returnOk $ InvokePage $ PageRemap asid' entries
-        odE
-    else  throwError TruncatedMessage
+    else throwError TruncatedMessage
     else if invocation_type label = ArchInvocationLabel ARMPageUnmap
     then  returnOk $ InvokePage $ PageUnmap cap cte
     else if isPageFlushLabel (invocation_type label) then
diff --git a/spec/abstract/ARM_HYP/ArchInvocation_A.thy b/spec/abstract/ARM_HYP/ArchInvocation_A.thy
index bc64d0954..873f3b6f9 100644
--- a/spec/abstract/ARM_HYP/ArchInvocation_A.thy
+++ b/spec/abstract/ARM_HYP/ArchInvocation_A.thy
@@ -48,9 +48,6 @@ datatype page_invocation
          (page_map_cap: cap)
          (page_map_ct_slot: cslot_ptr)
          (page_map_entries: "pte \<times> (obj_ref list) + pde \<times> (obj_ref list)")
-     | PageRemap
-         (page_remap_asid: asid)
-         (page_remap_entries: "pte \<times> (obj_ref list) + pde \<times> (obj_ref list)")
      | PageUnmap
          (page_unmap_cap: arch_cap)
          (page_unmap_cap_slot: cslot_ptr)
diff --git a/spec/abstract/ARM_HYP/Arch_A.thy b/spec/abstract/ARM_HYP/Arch_A.thy
index f721509d3..3ab85319c 100644
--- a/spec/abstract/ARM_HYP/Arch_A.thy
+++ b/spec/abstract/ARM_HYP/Arch_A.thy
@@ -123,9 +123,7 @@ where
 
 
 text \<open>The Page capability confers the authority to map, unmap and flush the
-memory page. The remap system call is a convenience operation that ensures the
-page is mapped in the same location as this cap was previously used to map it
-in.\<close>
+  memory page.\<close>
 definition
 perform_page_invocation :: "page_invocation \<Rightarrow> (unit,'z::state_ext) s_monad" where
 "perform_page_invocation iv \<equiv> case iv of
@@ -149,22 +147,6 @@ perform_page_invocation :: "page_invocation \<Rightarrow> (unit,'z::state_ext) s
             if flush then (invalidate_tlb_by_asid asid) else return ()
         od
     od
-| PageRemap asid (Inl (pte, slots)) \<Rightarrow> do
-    flush \<leftarrow> pte_check_if_mapped (hd slots);
-    store_pte (hd slots) pte;
-    mapM_x (swp store_pte InvalidPTE) (tl slots);
-    do_machine_op $ cleanCacheRange_PoU (hd slots) (last_byte_pte (last slots))
-                                        (addrFromPPtr (hd slots));
-    if flush then (invalidate_tlb_by_asid asid) else return ()
-  od
-| PageRemap asid (Inr (pde, slots)) \<Rightarrow> do
-    flush \<leftarrow> pde_check_if_mapped (hd slots);
-    store_pde (hd slots) pde;
-    mapM_x (swp store_pde InvalidPDE) (tl slots);
-    do_machine_op $ cleanCacheRange_PoU (hd slots) (last_byte_pde (last slots))
-                                        (addrFromPPtr (hd slots));
-    if flush then (invalidate_tlb_by_asid asid) else return ()
-  od
 | PageUnmap cap ct_slot \<Rightarrow>
     (case cap of
       PageCap dev p R vp_size vp_mapped_addr \<Rightarrow> do