2 files changed, 12 insertions, 12 deletions
diff --git a/src/gen_lib/sail2_prompt_monad.lem b/src/gen_lib/sail2_prompt_monad.lem
index e0ac09f6..28c0a27e 100644
--- a/src/gen_lib/sail2_prompt_monad.lem
+++ b/src/gen_lib/sail2_prompt_monad.lem
@@ -170,8 +170,8 @@ let read_mem_bytes rk addr sz =
     (maybe_fail "nat_of_bv" (nat_of_bv addr))
     (fun addr -> Read_mem rk addr (nat_of_int sz) return)
 
-val read_mem : forall 'rv 'a 'b 'e. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monad 'rv 'b 'e
-let read_mem rk addr sz =
+val read_mem : forall 'rv 'a 'b 'e 'addrsize. Bitvector 'a, Bitvector 'b => read_kind -> 'addrsize -> 'a -> integer -> monad 'rv 'b 'e
+let read_mem rk addr_sz addr sz =
   bind
     (read_mem_bytes rk addr sz)
     (fun bytes ->
@@ -185,15 +185,15 @@ let excl_result () =
   let k successful = (return successful) in
   Excl_res k
 
-val write_mem_ea : forall 'rv 'a 'e. Bitvector 'a => write_kind -> 'a -> integer -> monad 'rv unit 'e
-let write_mem_ea wk addr sz =
+val write_mem_ea : forall 'rv 'a 'e 'addrsize. Bitvector 'a => write_kind -> 'addrsize -> 'a -> integer -> monad 'rv unit 'e
+let write_mem_ea wk addr_size addr sz =
   bind
     (maybe_fail "nat_of_bv" (nat_of_bv addr))
     (fun addr -> Write_ea wk addr (nat_of_int sz) (Done ()))
 
-val write_mem : forall 'rv 'a 'b 'e. Bitvector 'a, Bitvector 'b =>
-  write_kind -> 'a -> integer -> 'b -> monad 'rv bool 'e
-let write_mem wk addr sz v =
+val write_mem : forall 'rv 'a 'b 'e 'addrsize. Bitvector 'a, Bitvector 'b =>
+  write_kind -> 'addrsize -> 'a -> integer -> 'b -> monad 'rv bool 'e
+let write_mem wk addr_size addr sz v =
   match (mem_bytes_of_bits v, nat_of_bv addr) with
     | (Just v, Just addr) ->
        Write_mem wk addr (nat_of_int sz) v return
diff --git a/src/gen_lib/sail2_state_monad.lem b/src/gen_lib/sail2_state_monad.lem
index 3042700c..8ea919f9 100644
--- a/src/gen_lib/sail2_state_monad.lem
+++ b/src/gen_lib/sail2_state_monad.lem
@@ -147,8 +147,8 @@ let read_memtS rk a sz =
   maybe_failS "bits_of_mem_bytes" (of_bits (bits_of_mem_bytes bytes)) >>$= (fun mem_val ->
   returnS (mem_val, tag))))
 
-val read_memS : forall 'regs 'e 'a 'b. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monadS 'regs 'b 'e
-let read_memS rk a sz =
+val read_memS : forall 'regs 'e 'a 'b 'addrsize. Bitvector 'a, Bitvector 'b => read_kind -> 'addrsize -> 'a -> integer -> monadS 'regs 'b 'e
+let read_memS rk addr_size a sz =
   read_memtS rk a sz >>$= (fun (bytes, _) ->
   returnS bytes)
 
@@ -186,9 +186,9 @@ let write_memtS wk addr sz v t =
     | _ -> failS "write_mem"
   end
 
-val write_memS : forall 'regs 'e 'a 'b. Bitvector 'a, Bitvector 'b =>
-  write_kind -> 'a -> integer -> 'b -> monadS 'regs bool 'e
-let write_memS wk addr sz v = write_memtS wk addr sz v B0
+val write_memS : forall 'regs 'e 'a 'b 'addrsize. Bitvector 'a, Bitvector 'b =>
+  write_kind -> 'addrsize -> 'a -> integer -> 'b -> monadS 'regs bool 'e
+let write_memS wk addr_size addr sz v = write_memtS wk addr sz v B0
 
 val read_regS : forall 'regs 'rv 'a 'e. register_ref 'regs 'rv 'a -> monadS 'regs 'a 'e
 let read_regS reg = readS (fun s -> reg.read_from s.regstate)