summaryrefslogtreecommitdiff
path: root/lib/hol
diff options
context:
space:
mode:
Diffstat (limited to 'lib/hol')
-rw-r--r--lib/hol/sail2_prompt_monad.lem2
1 files changed, 1 insertions, 1 deletions
diff --git a/lib/hol/sail2_prompt_monad.lem b/lib/hol/sail2_prompt_monad.lem
index ade12347..896c1a9c 100644
--- a/lib/hol/sail2_prompt_monad.lem
+++ b/lib/hol/sail2_prompt_monad.lem
@@ -44,7 +44,7 @@ let inline read_memt = read_memtS
let inline read_mem = read_memS
let inline excl_result = excl_resultS
let inline write_reg = write_regS
-let inline write_mem_ea wk addr sz = return ()
+let inline write_mem_ea wk addrsize addr sz = return ()
let inline write_memt = write_memtS
let inline write_mem = write_memS
let barrier _ = return ()