3 files changed, 8 insertions, 3 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 5f0f7478..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
@@ -46,5 +48,6 @@ 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
diff --git a/src/rewrites.ml b/src/rewrites.ml
index b47650b7..5a70a721 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -4012,12 +4012,13 @@ let rewrite_defs_remove_superfluous_letbinds env =
        | _ -> E_aux (exp,annot)
        end
     | E_internal_plet (_, E_aux (E_throw e, a), _) -> E_aux (E_throw e, a)
-    | E_internal_plet (_, E_aux (E_assert (c, msg), a), _) ->
+    | E_internal_plet (pat, (E_aux (E_assert (c, msg), a) as assert_exp), _) ->
        begin match typ_of c with
        | Typ_aux (Typ_app (Id_aux (Id "atom_bool", _), [A_aux (A_bool nc, _)]), _)
          when prove __POS__ (env_of c) (nc_not nc) ->
           (* Drop rest of block after an 'assert(false)' *)
-          E_aux (E_exit (infer_exp (env_of c) (mk_lit_exp L_unit)), a)
+          let exit_exp = E_aux (E_exit (infer_exp (env_of c) (mk_lit_exp L_unit)), a) in
+          E_aux (E_internal_plet (pat, assert_exp, exit_exp), annot)
        | _ ->
           E_aux (exp, annot)
        end