diff --git a/spec/haskell/src/SEL4/Kernel/VSpace/AARCH64.hs b/spec/haskell/src/SEL4/Kernel/VSpace/AARCH64.hs
index d9e321c53..6a6228ab5 100644
--- a/spec/haskell/src/SEL4/Kernel/VSpace/AARCH64.hs
+++ b/spec/haskell/src/SEL4/Kernel/VSpace/AARCH64.hs
@@ -461,12 +461,10 @@ isVTableRoot :: Capability -> Bool
 isVTableRoot (ArchObjectCap (PageTableCap { capPTType = VSRootPT_T })) = True
 isVTableRoot _ = False
 
--- FIXME AARCH64: name indirection kept here for sync with C; both (C and
--- Haskell) should define isValidVTableRoot directly
-isValidNativeRoot :: Capability -> Bool
-isValidNativeRoot cap = isVTableRoot cap && isJust (capPTMappedAddress (capCap cap))
+isValidVTableRoot :: Capability -> Bool
+isValidVTableRoot cap = isVTableRoot cap && isJust (capPTMappedAddress (capCap cap))
 
--- if isValidNativeRoot holds, return VSpace and ASID, otherwise throw error
+-- if isValidVTableRoot holds, return VSpace and ASID, otherwise throw error
 checkVSpaceRoot :: Capability  -> Int -> KernelF SyscallError (PPtr PTE, ASID)
 checkVSpaceRoot vspaceCap argNo =
     case vspaceCap of
@@ -476,9 +474,6 @@ checkVSpaceRoot vspaceCap argNo =
             -> return (vspace, asid)
         _ -> throw $ InvalidCapability argNo
 
-isValidVTableRoot :: Capability -> Bool
-isValidVTableRoot = isValidNativeRoot
-
 checkValidIPCBuffer :: VPtr -> Capability -> KernelF SyscallError ()
 checkValidIPCBuffer vptr (ArchObjectCap (FrameCap {capFIsDevice = False})) = do
     when (vptr .&. mask ipcBufferSizeBits /= 0) $ throw AlignmentError