Fix handling of E_internal_plet in rewrite

1 files changed, 11 insertions, 11 deletions

diff --git a/src/rewrites.ml b/src/rewrites.ml
index c9eece20..64cfe48b 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -3662,19 +3662,19 @@ let rewrite_defs_remove_superfluous_letbinds env =
          when Id.compare id id' = 0 && small exp1 && not (effectful exp1) ->
           let (E_aux (_,e1annot)) = exp1 in
           E_aux (E_internal_return (exp1),e1annot)
+       | _, (E_aux (E_throw e, a), _), _ -> E_aux (E_throw e, a)
+       | (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)' *)
+             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
        | _ -> E_aux (exp,annot)
        end
-    | E_internal_plet (_, E_aux (E_throw e, a), _) -> E_aux (E_throw e, 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)' *)
-          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
     | _ -> E_aux (exp,annot) in
 
   let alg = { id_exp_alg with e_aux = e_aux } in