diff --git a/haskell/src/SEL4/Kernel/VSpace/ARM.lhs b/haskell/src/SEL4/Kernel/VSpace/ARM.lhs
index 07b7b70621513a8fed95f7d5065129acf389c8da..61b8d522181ec570881e7f2ea9d43264dddcd38e 100644
--- a/haskell/src/SEL4/Kernel/VSpace/ARM.lhs
+++ b/haskell/src/SEL4/Kernel/VSpace/ARM.lhs
@@ -1093,9 +1093,7 @@ Capabilities for page directories --- the top level of the hardware-defined page
 >                 -- Fail if there is nothing mapped here
 >                 Nothing -> return $ InvokePageDirectory PageDirectoryNothing
 >                 Just frameInfo -> do
->                     withoutFailure $ stateAssert 
->                         (validMappingSize (fst frameInfo))
->                         "mapping found in PD is of invalid size"
+>                     withoutFailure $ checkValidMappingSize (fst frameInfo)
 >                     let baseStart = pageBase (VPtr start) (fst frameInfo)
 >                     let baseEnd = pageBase (VPtr end - 1) (fst frameInfo)
 >                     when (baseStart /= baseEnd) $
@@ -1313,8 +1311,8 @@ When we fetch a mapping in which to perform a page flush, we assert that its
 size is valid. This check is ignored in Haskell, but the Isabelle model has a
 notion of the largest permitted object size, and checks it appropriately.
 
-> validMappingSize :: VMPageSize -> KernelState -> Bool
-> validMappingSize _ = const True
+> checkValidMappingSize :: VMPageSize -> Kernel ()
+> checkValidMappingSize _ = return ()
 
 \subsection{Invocation Implementations}
 
diff --git a/haskell/src/SEL4/Object/TCB.lhs b/haskell/src/SEL4/Object/TCB.lhs
index e551f4f0ef592bc0f22aa7be23e03fc119cc4e9e..43ff275ccb90d76285f9ead13198d8df6ea22a98 100644
--- a/haskell/src/SEL4/Object/TCB.lhs
+++ b/haskell/src/SEL4/Object/TCB.lhs
@@ -587,7 +587,7 @@ When a new "Wait" operation begins, the caller slot in the waiting thread's TCB
 > deleteCallerCap receiver = do
 >     callerSlot <- getThreadCallerSlot receiver
 >     callerCap <- getSlotCap callerSlot
->     assert (isReplyCap callerCap || callerCap == NullCap)
+>     assert (isReplyCap callerCap || isNullCap callerCap)
 >         "Caller cap must be a reply cap"
 >     cteDeleteOne callerSlot