2 files changed, 10 insertions, 5 deletions
diff --git a/lib/hol/sail2_prompt.lem b/lib/hol/sail2_prompt.lem
index 674d4e34..3107d3a5 100644
--- a/lib/hol/sail2_prompt.lem
+++ b/lib/hol/sail2_prompt.lem
@@ -4,12 +4,13 @@ open import Sail2_state
 
 let inline undefined_bool = undefined_boolS
 let inline bool_of_bitU_nondet = bool_of_bitU_nondetS
-let inline bool_of_bitU_fail = bool_of_bitU_fail
+let inline bool_of_bitU_fail = Sail2_state.bool_of_bitU_fail
 let inline bools_of_bits_nondet = bools_of_bits_nondetS
 let inline of_bits_nondet = of_bits_nondetS
 let inline of_bits_fail = of_bits_failS
 let inline mword_nondet = mword_nondetS
 let inline reg_deref = read_regS
+let inline choose msg xs = chooseS xs
 let inline internal_pick = internal_pickS
 
 let inline foreachM = foreachS
diff --git a/lib/hol/sail2_prompt_monad.lem b/lib/hol/sail2_prompt_monad.lem
index 3af931a5..ade12347 100644
--- a/lib/hol/sail2_prompt_monad.lem
+++ b/lib/hol/sail2_prompt_monad.lem
@@ -22,6 +22,8 @@ let inline bind = bindS
 let inline (>>=) = (>>$=)
 let inline (>>) = (>>$)
 
+let inline choose_bool msg = choose_boolS ()
+let inline undefined_bool = undefined_boolS
 let inline exit = exitS
 
 let inline throw = throwS
@@ -34,16 +36,18 @@ let inline try_catchR = try_catchRS
 
 let inline maybe_fail = maybe_failS
 
+let inline read_memt_bytes = read_memt_bytesS
 let inline read_mem_bytes = read_mem_bytesS
 let inline read_reg = read_regS
 let inline reg_deref = read_regS
+let inline read_memt = read_memtS
 let inline read_mem = read_memS
-let inline read_tag = read_tagS
 let inline excl_result = excl_resultS
 let inline write_reg = write_regS
-let inline write_tag = write_tagS
-let inline write_mem_ea wk addr sz = write_mem_eaS wk addr (nat_of_int sz)
-let inline write_mem_val = write_mem_valS
+let inline write_mem_ea wk addr sz = return ()
+let inline write_memt = write_memtS
+let inline write_mem = write_memS
 let barrier _ = return ()
+let footprint _ = return ()
 
 let inline assert_exp = assert_expS