Remove FES_Fexps constructor

This makes dealing with records and field expressions in Sail much
nicer because the constructors are no longer stacked together like
matryoshka dolls with unnecessary layers. Previously to get the fields
of a record it would be either

E_aux (E_record (FES_aux (FES_Fexps (fexps, _), _)), _)

but now it is simply:

E_aux (E_record fexps, _)

16 files changed, 91 insertions, 127 deletions

diff --git a/src/anf.ml b/src/anf.ml
index 1f93e00f..915ab738 100644
--- a/src/anf.ml
+++ b/src/anf.ml
@@ -569,7 +569,7 @@ let rec anf (E_aux (e_aux, ((l, _) as exp_annot)) as exp) =
      let aval, wrap = to_aval (anf field_exp) in
      wrap (mk_aexp (AE_field (aval, id, typ_of exp)))
 
-  | E_record_update (exp, FES_aux (FES_Fexps (fexps, _), _)) ->
+  | E_record_update (exp, fexps) ->
      let anf_fexp (FE_aux (FE_Fexp (id, exp), _)) =
        let aval, wrap = to_aval (anf exp) in
        (id, aval), wrap
@@ -679,7 +679,7 @@ let rec anf (E_aux (e_aux, ((l, _) as exp_annot)) as exp) =
      let wrap = List.fold_left (fun f g x -> f (g x)) (fun x -> x) (List.map snd avals) in
      wrap (mk_aexp (AE_val (AV_tuple (List.map fst avals))))
 
-  | E_record (FES_aux (FES_Fexps (fexps, _), _)) ->
+  | E_record fexps ->
      let anf_fexp (FE_aux (FE_Fexp (id, exp), _)) =
        let aval, wrap = to_aval (anf exp) in
        (id, aval), wrap
diff --git a/src/ast_util.ml b/src/ast_util.ml
index ffe4c90e..48750ab7 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -393,7 +393,6 @@ let mk_typschm typq typ = TypSchm_aux (TypSchm_ts (typq, typ), Parse_ast.Unknown
 let mk_typquant qis = TypQ_aux (TypQ_tq qis, Parse_ast.Unknown)
 
 let mk_fexp id exp = FE_aux (FE_Fexp (id, exp), no_annot)
-let mk_fexps fexps = FES_aux (FES_Fexps (fexps, false), no_annot)
 
 let mk_effect effs =
   Effect_aux (Effect_set (List.map (fun be_aux -> BE_aux (be_aux, Parse_ast.Unknown)) effs), Parse_ast.Unknown)
@@ -461,8 +460,8 @@ and map_exp_annot_aux f = function
   | E_vector_append (exp1, exp2) -> E_vector_append (map_exp_annot f exp1, map_exp_annot f exp2)
   | E_list xs -> E_list (List.map (map_exp_annot f) xs)
   | E_cons (exp1, exp2) -> E_cons (map_exp_annot f exp1, map_exp_annot f exp2)
-  | E_record fexps -> E_record (map_fexps_annot f fexps)
-  | E_record_update (exp, fexps) -> E_record_update (map_exp_annot f exp, map_fexps_annot f fexps)
+  | E_record fexps -> E_record (List.map (map_fexp_annot f) fexps)
+  | E_record_update (exp, fexps) -> E_record_update (map_exp_annot f exp, List.map (map_fexp_annot f) fexps)
   | E_field (exp, id) -> E_field (map_exp_annot f exp, id)
   | E_case (exp, cases) -> E_case (map_exp_annot f exp, List.map (map_pexp_annot f) cases)
   | E_try (exp, cases) -> E_try (map_exp_annot f exp, List.map (map_pexp_annot f) cases)
@@ -482,7 +481,6 @@ and map_opt_default_annot f (Def_val_aux (df, annot)) = Def_val_aux (map_opt_def
 and map_opt_default_annot_aux f = function
   | Def_val_empty -> Def_val_empty
   | Def_val_dec exp -> Def_val_dec (map_exp_annot f exp)
-and map_fexps_annot f (FES_aux (FES_Fexps (fexps, b), annot)) = FES_aux (FES_Fexps (List.map (map_fexp_annot f) fexps, b), f annot)
 and map_fexp_annot f (FE_aux (FE_Fexp (id, exp), annot)) = FE_aux (FE_Fexp (id, map_exp_annot f exp), f annot)
 and map_pexp_annot f (Pat_aux (pexp, annot)) = Pat_aux (map_pexp_annot_aux f pexp, f annot)
 and map_pexp_annot_aux f = function
@@ -770,9 +768,9 @@ let rec string_of_exp (E_aux (exp, _)) =
   | E_throw exp -> "throw " ^ string_of_exp exp
   | E_cons (x, xs) -> string_of_exp x ^ " :: " ^ string_of_exp xs
   | E_list xs -> "[|" ^ string_of_list ", " string_of_exp xs ^ "|]"
-  | E_record_update (exp, FES_aux (FES_Fexps (fexps, _), _)) ->
+  | E_record_update (exp, fexps) ->
      "{ " ^ string_of_exp exp ^ " with " ^ string_of_list "; " string_of_fexp fexps ^ " }"
-  | E_record (FES_aux (FES_Fexps (fexps, _), _)) ->
+  | E_record fexps ->
      "{ " ^ string_of_list "; " string_of_fexp fexps ^ " }"
   | E_var (lexp, binding, exp) -> "var " ^ string_of_lexp lexp ^ " = " ^ string_of_exp binding ^ " in " ^ string_of_exp exp
   | E_internal_return exp -> "internal_return (" ^ string_of_exp exp ^ ")"
@@ -1290,8 +1288,8 @@ let rec subst id value (E_aux (e_aux, annot) as exp) =
     | E_list exps -> E_list (List.map (subst id value) exps)
     | E_cons (exp1, exp2) -> E_cons (subst id value exp1, subst id value exp2)
 
-    | E_record fexps -> E_record (subst_fexps id value fexps)
-    | E_record_update (exp, fexps) -> E_record_update (subst id value exp, subst_fexps id value fexps)
+    | E_record fexps -> E_record (List.map (subst_fexp id value) fexps)
+    | E_record_update (exp, fexps) -> E_record_update (subst id value exp, List.map (subst_fexp id value) fexps)
     | E_field (exp, id') -> E_field (subst id value exp, id')
 
     | E_case (exp, pexps) ->
@@ -1336,10 +1334,6 @@ and subst_pexp id value (Pat_aux (pexp_aux, annot)) =
   in
   Pat_aux (pexp_aux, annot)
 
-
-and subst_fexps id value (FES_aux (FES_Fexps (fexps, flag), annot)) =
-  FES_aux (FES_Fexps (List.map (subst_fexp id value) fexps, flag), annot)
-
 and subst_fexp id value (FE_aux (FE_Fexp (id', exp), annot)) =
   FE_aux (FE_Fexp (id', subst id value exp), annot)
 
@@ -1493,8 +1487,8 @@ let rec locate : 'a. (l -> l) -> 'a exp -> 'a exp = fun f (E_aux (e_aux, (l, ann
        E_vector_append (locate f exp1, locate f exp2)
     | E_list exps -> E_list (List.map (locate f) exps)
     | E_cons (exp1, exp2) -> E_cons (locate f exp1, locate f exp2)
-    | E_record fexps -> E_record (locate_fexps f fexps)
-    | E_record_update (exp, fexps) -> E_record_update (locate f exp, locate_fexps f fexps)
+    | E_record fexps -> E_record (List.map (locate_fexp f) fexps)
+    | E_record_update (exp, fexps) -> E_record_update (locate f exp, List.map (locate_fexp f) fexps)
     | E_field (exp, id) -> E_field (locate f exp, locate_id f id)
     | E_case (exp, cases) -> E_case (locate f exp, List.map (locate_pexp f) cases)
     | E_let (letbind, exp) -> E_let (locate_letbind f letbind, locate f exp)
@@ -1538,9 +1532,6 @@ and locate_lexp : 'a. (l -> l) -> 'a lexp -> 'a lexp = fun f (LEXP_aux (lexp_aux
   in
   LEXP_aux (lexp_aux, (f l, annot))
 
-and locate_fexps : 'a. (l -> l) -> 'a fexps -> 'a fexps = fun f (FES_aux (FES_Fexps (fexps, semi), (l, annot))) ->
-  FES_aux (FES_Fexps (List.map (locate_fexp f) fexps, semi), (f l, annot))
-
 and locate_fexp : 'a. (l -> l) -> 'a fexp -> 'a fexp = fun f (FE_aux (FE_Fexp (id, exp), (l, annot))) ->
   FE_aux (FE_Fexp (locate_id f id, locate f exp), (f l, annot))
 
diff --git a/src/ast_util.mli b/src/ast_util.mli
index b7979e88..b6bce7c5 100644
--- a/src/ast_util.mli
+++ b/src/ast_util.mli
@@ -89,7 +89,6 @@ val mk_qi_id : kind_aux -> kid -> quant_item
 val mk_qi_nc : n_constraint -> quant_item
 val mk_qi_kopt : kinded_id -> quant_item
 val mk_fexp : id -> unit exp -> unit fexp
-val mk_fexps : (unit fexp) list -> unit fexps
 val mk_letbind : unit pat -> unit exp -> unit letbind
 
 val unaux_exp : 'a exp -> 'a exp_aux
diff --git a/src/constant_fold.ml b/src/constant_fold.ml
index 0e34ed5b..b86f4ea5 100644
--- a/src/constant_fold.ml
+++ b/src/constant_fold.ml
@@ -72,7 +72,7 @@ and exp_of_value =
   | V_bool false -> mk_lit_exp L_false
   | V_string str -> mk_lit_exp (L_string str)
   | V_record ctors ->
-     mk_exp (E_record (FES_aux (FES_Fexps (List.map fexp_of_ctor (StringMap.bindings ctors), false), no_annot)))
+     mk_exp (E_record (List.map fexp_of_ctor (StringMap.bindings ctors)))
   | V_vector vs ->
      mk_exp (E_vector (List.map exp_of_value vs))
   | V_tuple vs ->
@@ -110,7 +110,7 @@ let rec is_constant (E_aux (e_aux, _)) =
   match e_aux with
   | E_lit _ -> true
   | E_vector exps -> List.for_all is_constant exps
-  | E_record (FES_aux (FES_Fexps (fexps, _), _)) -> List.for_all is_constant_fexp fexps
+  | E_record fexps -> List.for_all is_constant_fexp fexps
   | E_cast (_, exp) -> is_constant exp
   | E_tuple exps -> List.for_all is_constant exps
   | _ -> false
diff --git a/src/initial_check.ml b/src/initial_check.ml
index d1efb374..aa3a7136 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -595,14 +595,14 @@ and to_ast_case (k_env : kind Envmap.t) (def_ord : order) (Parse_ast.Pat_aux(pex
   | Parse_ast.Pat_when(pat,guard,exp) ->
      Pat_aux (Pat_when (to_ast_pat k_env def_ord pat, to_ast_exp k_env def_ord guard, to_ast_exp k_env def_ord exp), (l, ()))
 
-and to_ast_fexps (fail_on_error:bool) (k_env:kind Envmap.t) (def_ord:order) (exps : Parse_ast.exp list) : unit fexps option =
+and to_ast_fexps (fail_on_error:bool) (k_env:kind Envmap.t) (def_ord:order) (exps : Parse_ast.exp list) : unit fexp list option =
   match exps with
-  | [] -> Some(FES_aux(FES_Fexps([],false), (Parse_ast.Unknown,())))
+  | [] -> Some []
   | fexp::exps -> let maybe_fexp,maybe_error = to_ast_record_try k_env def_ord fexp in
                   (match maybe_fexp,maybe_error with
                   | Some(fexp),None ->
                     (match (to_ast_fexps fail_on_error k_env def_ord exps) with
-                    | Some(FES_aux(FES_Fexps(fexps,_),l)) -> Some(FES_aux(FES_Fexps(fexp::fexps,false),l))
+                    | Some(fexps) -> Some(fexp::fexps)
                     | _  -> None)
                   | None,Some(l,msg) ->
                     if fail_on_error
@@ -1138,7 +1138,7 @@ let generate_undefineds vs_ids (Defs defs) =
        [mk_val_spec (VS_val_spec (undefined_typschm id typq, prepend_id "undefined_" id, (fun _ -> None), false));
         mk_fundef [mk_funcl (prepend_id "undefined_" id)
                             pat
-                            (mk_exp (E_record (mk_fexps (List.map (fun (_, id) -> mk_fexp id (mk_lit_exp L_undef)) fields))))]]
+                            (mk_exp (E_record (List.map (fun (_, id) -> mk_fexp id (mk_lit_exp L_undef)) fields)))]]
     | TD_variant (id, _, typq, tus, _) when not (IdSet.mem (prepend_id "undefined_" id) vs_ids) ->
        let pat = p_tup (quant_items typq |> List.map quant_item_param |> List.concat |> List.map (fun id -> mk_pat (P_id id))) in
        let body =
diff --git a/src/interpreter.ml b/src/interpreter.ml
index 03877600..194812ca 100644
--- a/src/interpreter.ml
+++ b/src/interpreter.ml
@@ -401,13 +401,13 @@ let rec step (E_aux (e_aux, annot) as orig_exp) =
        | _ -> failwith ("Couldn't find id " ^ string_of_id id)
      end
 
-  | E_record (FES_aux (FES_Fexps (fexps, flag), fes_annot)) ->
+  | E_record fexps ->
      let evaluated, unevaluated = Util.take_drop is_value_fexp fexps in
      begin
        match unevaluated with
        | FE_aux (FE_Fexp (id, exp), fe_annot) :: fexps ->
           step exp >>= fun exp' ->
-          wrap (E_record (FES_aux (FES_Fexps (evaluated @ FE_aux (FE_Fexp (id, exp'), fe_annot) :: fexps, flag), fes_annot)))
+          wrap (E_record (evaluated @ FE_aux (FE_Fexp (id, exp'), fe_annot) :: fexps))
        | [] ->
           List.map value_of_fexp fexps
           |> List.fold_left (fun record (field, v) -> StringMap.add field v record) StringMap.empty
@@ -418,13 +418,13 @@ let rec step (E_aux (e_aux, annot) as orig_exp) =
 
   | E_record_update (exp, fexps) when not (is_value exp) ->
      step exp >>= fun exp' -> wrap (E_record_update (exp', fexps))
-  | E_record_update (record, FES_aux (FES_Fexps (fexps, flag), fes_annot)) ->
+  | E_record_update (record, fexps) ->
      let evaluated, unevaluated = Util.take_drop is_value_fexp fexps in
      begin
        match unevaluated with
        | FE_aux (FE_Fexp (id, exp), fe_annot) :: fexps ->
           step exp >>= fun exp' ->
-          wrap (E_record_update (record, FES_aux (FES_Fexps (evaluated @ FE_aux (FE_Fexp (id, exp'), fe_annot) :: fexps, flag), fes_annot)))
+          wrap (E_record_update (record, evaluated @ FE_aux (FE_Fexp (id, exp'), fe_annot) :: fexps))
        | [] ->
           List.map value_of_fexp fexps
           |> List.fold_left (fun record (field, v) -> StringMap.add field v record) (coerce_record (value_of_exp record))
@@ -444,7 +444,7 @@ let rec step (E_aux (e_aux, annot) as orig_exp) =
   | E_assign (LEXP_aux (LEXP_field (lexp, id), ul), exp) ->
      let open Type_check in
      let lexp_exp = infer_exp (env_of_annot annot) (exp_of_lexp (strip_lexp lexp)) in
-     let exp' = E_aux (E_record_update (lexp_exp, FES_aux (FES_Fexps ([FE_aux (FE_Fexp (id, exp), ul)], false), ul)), ul) in
+     let exp' = E_aux (E_record_update (lexp_exp, [FE_aux (FE_Fexp (id, exp), ul)]), ul) in
      wrap (E_assign (lexp, exp'))
   | E_assign (LEXP_aux (LEXP_vector (vec, n), lexp_annot), exp) ->
      let open Type_check in
diff --git a/src/monomorphise.ml b/src/monomorphise.ml
index 6a262df6..7626971e 100644
--- a/src/monomorphise.ml
+++ b/src/monomorphise.ml
@@ -615,8 +615,8 @@ let nexp_subst_fns substs =
       | E_vector_append (e1,e2) -> re (E_vector_append (s_exp e1,s_exp e2))
       | E_list es -> re (E_list (List.map s_exp es))
       | E_cons (e1,e2) -> re (E_cons (s_exp e1,s_exp e2))
-      | E_record fes -> re (E_record (s_fexps fes))
-      | E_record_update (e,fes) -> re (E_record_update (s_exp e, s_fexps fes))
+      | E_record fes -> re (E_record (List.map s_fexp fes))
+      | E_record_update (e,fes) -> re (E_record_update (s_exp e, List.map s_fexp fes))
       | E_field (e,id) -> re (E_field (s_exp e,id))
       | E_case (e,cases) -> re (E_case (s_exp e, List.map s_pexp cases))
       | E_let (lb,e) -> re (E_let (s_letbind lb, s_exp e))
@@ -629,8 +629,6 @@ let nexp_subst_fns substs =
       | E_internal_return e -> re (E_internal_return (s_exp e))
       | E_throw e -> re (E_throw (s_exp e))
       | E_try (e,cases) -> re (E_try (s_exp e, List.map s_pexp cases))
-    and s_fexps (FES_aux (FES_Fexps (fes,flag), (l,annot))) =
-      FES_aux (FES_Fexps (List.map s_fexp fes, flag), (l,s_tannot annot))
     and s_fexp (FE_aux (FE_Fexp (id,e), (l,annot))) =
       FE_aux (FE_Fexp (id,s_exp e),(l,s_tannot annot))
     and s_pexp = function
@@ -954,7 +952,7 @@ let referenced_vars exp =
          { (compute_exp_alg IdSet.empty IdSet.union) with
            e_ref = (fun id -> IdSet.singleton id, E_ref id) } exp)
 
-let assigned_vars_in_fexps (FES_aux (FES_Fexps (fes,_), _)) =
+let assigned_vars_in_fexps fes =
   List.fold_left
     (fun vs (FE_aux (FE_Fexp (_,e),_)) -> IdSet.union vs (assigned_vars e))
     IdSet.empty
@@ -1460,8 +1458,8 @@ let split_defs all_errors splits defs =
     | E_internal_value _
       -> raise (Reporting.err_unreachable l __POS__
                   ("Unexpected expression encountered in monomorphisation: " ^ string_of_exp exp))
-  and const_prop_fexps ref_vars substs assigns (FES_aux (FES_Fexps (fes,flag), annot)) =
-    FES_aux (FES_Fexps (List.map (const_prop_fexp ref_vars substs assigns) fes, flag), annot)
+  and const_prop_fexps ref_vars substs assigns fes =
+    List.map (const_prop_fexp ref_vars substs assigns) fes
   and const_prop_fexp ref_vars substs assigns (FE_aux (FE_Fexp (id,e), annot)) =
     FE_aux (FE_Fexp (id,fst (const_prop_exp ref_vars substs assigns e)),annot)
   and const_prop_pexp ref_vars substs assigns = function
@@ -1995,8 +1993,8 @@ let split_defs all_errors splits defs =
         | E_vector_append (e1,e2) -> re (E_vector_append (map_exp e1,map_exp e2))
         | E_list es -> re (E_list (List.map map_exp es))
         | E_cons (e1,e2) -> re (E_cons (map_exp e1,map_exp e2))
-        | E_record fes -> re (E_record (map_fexps fes))
-        | E_record_update (e,fes) -> re (E_record_update (map_exp e, map_fexps fes))
+        | E_record fes -> re (E_record (List.map map_fexp fes))
+        | E_record_update (e,fes) -> re (E_record_update (map_exp e, List.map map_fexp fes))
         | E_field (e,id) -> re (E_field (map_exp e,id))
         | E_case (e,cases) -> re (E_case (map_exp e, List.concat (List.map map_pexp cases)))
         | E_let (lb,e) -> re (E_let (map_letbind lb, map_exp e))
@@ -2009,8 +2007,6 @@ let split_defs all_errors splits defs =
         | E_var (le,e1,e2) -> re (E_var (map_lexp le, map_exp e1, map_exp e2))
         | E_internal_plet (p,e1,e2) -> re (E_internal_plet (check_single_pat p, map_exp e1, map_exp e2))
         | E_internal_return e -> re (E_internal_return (map_exp e))
-      and map_fexps (FES_aux (FES_Fexps (fes,flag), annot)) =
-        FES_aux (FES_Fexps (List.map map_fexp fes, flag), annot)
       and map_fexp (FE_aux (FE_Fexp (id,e), annot)) =
         FE_aux (FE_Fexp (id,map_exp e),annot)
       and map_pexp = function
@@ -3087,11 +3083,11 @@ let rec analyse_exp fn_id env assigns (E_aux (e,(l,annot)) as exp) =
     | E_vector_update_subrange (e1,e2,e3,e4) ->
        let ds, assigns, r = non_det [e1;e2;e3;e4] in
        (merge_deps ds, assigns, r)
-    | E_record (FES_aux (FES_Fexps (fexps,_),_)) ->
+    | E_record fexps ->
        let es = List.map (function (FE_aux (FE_Fexp (_,e),_)) -> e) fexps in
        let ds, assigns, r = non_det es in
        (merge_deps ds, assigns, r)
-    | E_record_update (e,FES_aux (FES_Fexps (fexps,_),_)) ->
+    | E_record_update (e,fexps) ->
        let es = List.map (function (FE_aux (FE_Fexp (_,e),_)) -> e) fexps in
        let ds, assigns, r = non_det (e::es) in
        (merge_deps ds, assigns, r)
diff --git a/src/ocaml_backend.ml b/src/ocaml_backend.ml
index cf681ae5..f3a3fa54 100644
--- a/src/ocaml_backend.ml
+++ b/src/ocaml_backend.ml
@@ -242,9 +242,9 @@ let rec ocaml_exp ctx (E_aux (exp_aux, _) as exp) =
   | E_if (c, t, e) -> separate space [string "if"; ocaml_atomic_exp ctx c;
                                       string "then"; ocaml_atomic_exp ctx t;
                                       string "else"; ocaml_atomic_exp ctx e]
-  | E_record (FES_aux (FES_Fexps (fexps, _), _)) ->
+  | E_record fexps ->
      enclose lbrace rbrace (group (separate_map (semi ^^ break 1) (ocaml_fexp ctx) fexps))
-  | E_record_update (exp, FES_aux (FES_Fexps (fexps, _), _)) ->
+  | E_record_update (exp, fexps) ->
      enclose lbrace rbrace (separate space [ocaml_atomic_exp ctx exp;
                                             string "with";
                                             separate_map (semi ^^ space) (ocaml_fexp ctx) fexps])
diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index 4b466326..7cc61507 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -1370,7 +1370,7 @@ let doc_exp, doc_let =
        if aexp_needed then parens epp else epp
     | E_tuple exps ->
        parens (align (group (separate_map (comma ^^ break 1) expN exps)))
-    | E_record(FES_aux(FES_Fexps(fexps,_),_)) ->
+    | E_record fexps ->
        let recordtyp = match destruct_tannot annot with
          | Some (env, Typ_aux (Typ_id tid,_), _)
          | Some (env, Typ_aux (Typ_app (tid, _), _), _) ->
@@ -1381,7 +1381,7 @@ let doc_exp, doc_let =
                                           (semi_sp ^^ break 1)
                                           (doc_fexp ctxt recordtyp) fexps)) in
        if aexp_needed then parens epp else epp
-    | E_record_update(e,(FES_aux(FES_Fexps(fexps,_),_))) ->
+    | E_record_update(e, fexps) ->
        let recordtyp, env = match destruct_tannot annot with
          | Some (env, Typ_aux (Typ_id tid,_), _)
          | Some (env, Typ_aux (Typ_app (tid, _), _), _)
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index 53b703bf..be790a1c 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -825,7 +825,7 @@ let doc_exp_lem, doc_let_lem =
     | E_cast(typ,e) -> expV aexp_needed e
     | E_tuple exps ->
        parens (align (group (separate_map (comma ^^ break 1) expN exps)))
-    | E_record(FES_aux(FES_Fexps(fexps,_),_)) ->
+    | E_record fexps ->
        let recordtyp = match destruct_tannot annot with
          | Some (env, Typ_aux (Typ_id tid,_), _)
          | Some (env, Typ_aux (Typ_app (tid, _), _), _) ->
@@ -835,7 +835,7 @@ let doc_exp_lem, doc_let_lem =
        wrap_parens (anglebars (space ^^ (align (separate_map
                                         (semi_sp ^^ break 1)
                                         (doc_fexp ctxt recordtyp) fexps)) ^^ space))
-    | E_record_update(e,(FES_aux(FES_Fexps(fexps,_),_))) ->
+    | E_record_update(e, fexps) ->
        let recordtyp = match destruct_tannot annot with
          | Some (env, Typ_aux (Typ_id tid,_), _)
          | Some (env, Typ_aux (Typ_app (tid, _), _), _)
diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml
index fe533f00..b1efd11d 100644
--- a/src/pretty_print_sail.ml
+++ b/src/pretty_print_sail.ml
@@ -453,7 +453,7 @@ and doc_atomic_exp (E_aux (e_aux, _) as exp) =
      brackets (separate space [doc_exp exp1; string "with"; doc_atomic_exp exp2; string ".."; doc_atomic_exp exp3; equals; doc_exp exp4])
   | E_internal_value v -> string (Value.string_of_value v |> Util.green |> Util.clear)
   | _ -> parens (doc_exp exp)
-and doc_fexps (FES_aux (FES_Fexps (fexps, _), _)) =
+and doc_fexps fexps =
   separate_map (comma ^^ space) doc_fexp fexps
 and doc_fexp (FE_aux (FE_Fexp (id, exp), _)) =
   separate space [doc_id id; equals; doc_exp exp]
diff --git a/src/rewriter.ml b/src/rewriter.ml
index 082d9850..77070025 100644
--- a/src/rewriter.ml
+++ b/src/rewriter.ml
@@ -64,11 +64,10 @@ type 'a rewriters = {
     rewrite_defs : 'a rewriters -> 'a defs -> 'a defs;
   }
 
-
 let effect_of_fpat (FP_aux (_,(_,a))) = effect_of_annot a
 let effect_of_lexp (LEXP_aux (_,(_,a))) = effect_of_annot a
 let effect_of_fexp (FE_aux (_,(_,a))) = effect_of_annot a
-let effect_of_fexps (FES_aux (FES_Fexps (fexps,_),_)) =
+let effect_of_fexps fexps =
   List.fold_left union_effects no_effect (List.map effect_of_fexp fexps)
 let effect_of_opt_default (Def_val_aux (_,(_,a))) = effect_of_annot a
 (* The typechecker does not seem to annotate pexps themselves *)
@@ -295,16 +294,14 @@ let rewrite_exp rewriters (E_aux (exp,(l,annot)) as orig_exp) =
   | E_vector_append (v1,v2) -> rewrap (E_vector_append (rewrite v1,rewrite v2))
   | E_list exps -> rewrap (E_list (List.map rewrite exps))
   | E_cons(h,t) -> rewrap (E_cons (rewrite h,rewrite t))
-  | E_record (FES_aux (FES_Fexps(fexps, bool),fannot)) ->
+  | E_record fexps ->
     rewrap (E_record
-              (FES_aux (FES_Fexps
-                          (List.map (fun (FE_aux(FE_Fexp(id,e),fannot)) ->
-                               FE_aux(FE_Fexp(id,rewrite e),fannot)) fexps, bool), fannot)))
-  | E_record_update (re,(FES_aux (FES_Fexps(fexps, bool),fannot))) ->
+              (List.map (fun (FE_aux(FE_Fexp(id,e),fannot)) ->
+                   FE_aux(FE_Fexp(id,rewrite e),fannot)) fexps))
+  | E_record_update (re, fexps) ->
     rewrap (E_record_update ((rewrite re),
-                             (FES_aux (FES_Fexps
-                                         (List.map (fun (FE_aux(FE_Fexp(id,e),fannot)) ->
-                                              FE_aux(FE_Fexp(id,rewrite e),fannot)) fexps, bool), fannot))))
+                             (List.map (fun (FE_aux(FE_Fexp(id,e),fannot)) ->
+                                  FE_aux(FE_Fexp(id,rewrite e),fannot)) fexps)))
   | E_field(exp,id) -> rewrap (E_field(rewrite exp,id))
   | E_case (exp,pexps) ->
     rewrap (E_case (rewrite exp, List.map (rewrite_pexp rewriters) pexps))
@@ -475,9 +472,9 @@ let id_pat_alg : ('a,'a pat, 'a pat_aux, 'a fpat, 'a fpat_aux) pat_alg =
   ; fP_Fpat          = (fun (id,pat) -> FP_Fpat (id,pat))
   }
 
-type ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_aux,
+type ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,
       'opt_default_aux,'opt_default,'pexp,'pexp_aux,'letbind_aux,'letbind,
-      'pat,'pat_aux,'fpat,'fpat_aux) exp_alg = 
+      'pat,'pat_aux,'fpat,'fpat_aux) exp_alg =
   { e_block                  : 'exp list -> 'exp_aux
   ; e_nondet                 : 'exp list -> 'exp_aux
   ; e_id                     : id -> 'exp_aux
@@ -498,8 +495,8 @@ type ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_aux,
   ; e_vector_append          : 'exp * 'exp -> 'exp_aux
   ; e_list                   : 'exp list -> 'exp_aux
   ; e_cons                   : 'exp * 'exp -> 'exp_aux
-  ; e_record                 : 'fexps -> 'exp_aux
-  ; e_record_update          : 'exp * 'fexps -> 'exp_aux
+  ; e_record                 : 'fexp list -> 'exp_aux
+  ; e_record_update          : 'exp * 'fexp list -> 'exp_aux
   ; e_field                  : 'exp * id -> 'exp_aux
   ; e_case                   : 'exp * 'pexp list -> 'exp_aux
   ; e_try                    : 'exp * 'pexp list -> 'exp_aux
@@ -528,8 +525,6 @@ type ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_aux,
   ; lEXP_aux                 : 'lexp_aux * 'a annot -> 'lexp
   ; fE_Fexp                  : id * 'exp -> 'fexp_aux
   ; fE_aux                   : 'fexp_aux * 'a annot -> 'fexp
-  ; fES_Fexps                : 'fexp list * bool -> 'fexps_aux
-  ; fES_aux                  : 'fexps_aux * 'a annot -> 'fexps
   ; def_val_empty            : 'opt_default_aux
   ; def_val_dec              : 'exp -> 'opt_default_aux
   ; def_val_aux              : 'opt_default_aux * 'a annot -> 'opt_default
@@ -567,8 +562,8 @@ let rec fold_exp_aux alg = function
   | E_vector_append (e1,e2) -> alg.e_vector_append (fold_exp alg e1, fold_exp alg e2)
   | E_list es -> alg.e_list (List.map (fold_exp alg) es)
   | E_cons (e1,e2) -> alg.e_cons (fold_exp alg e1, fold_exp alg e2)
-  | E_record fexps -> alg.e_record (fold_fexps alg fexps)
-  | E_record_update (e,fexps) -> alg.e_record_update (fold_exp alg e, fold_fexps alg fexps)
+  | E_record fexps -> alg.e_record (List.map (fold_fexp alg) fexps)
+  | E_record_update (e,fexps) -> alg.e_record_update (fold_exp alg e, List.map (fold_fexp alg) fexps)
   | E_field (e,id) -> alg.e_field (fold_exp alg e, id)
   | E_case (e,pexps) -> alg.e_case (fold_exp alg e, List.map (fold_pexp alg) pexps)
   | E_try (e,pexps) -> alg.e_try (fold_exp alg e, List.map (fold_pexp alg) pexps)
@@ -602,8 +597,6 @@ and fold_lexp alg (LEXP_aux (lexp_aux,annot)) =
   alg.lEXP_aux (fold_lexp_aux alg lexp_aux, annot)
 and fold_fexp_aux alg (FE_Fexp (id,e)) = alg.fE_Fexp (id, fold_exp alg e)
 and fold_fexp alg (FE_aux (fexp_aux,annot)) = alg.fE_aux (fold_fexp_aux alg fexp_aux,annot)
-and fold_fexps_aux alg (FES_Fexps (fexps,b)) = alg.fES_Fexps (List.map (fold_fexp alg) fexps, b)
-and fold_fexps alg (FES_aux (fexps_aux,annot)) = alg.fES_aux (fold_fexps_aux alg fexps_aux, annot)
 and fold_opt_default_aux alg = function
   | Def_val_empty -> alg.def_val_empty
   | Def_val_dec e -> alg.def_val_dec (fold_exp alg e)
@@ -674,8 +667,6 @@ let id_exp_alg =
   ; lEXP_aux = (fun (lexp,annot) -> LEXP_aux (lexp,annot))
   ; fE_Fexp = (fun (id,e) -> FE_Fexp (id,e))
   ; fE_aux = (fun (fexp,annot) -> FE_aux (fexp,annot))
-  ; fES_Fexps = (fun (fexps,b) -> FES_Fexps (fexps,b))
-  ; fES_aux = (fun (fexp,annot) -> FES_aux (fexp,annot))
   ; def_val_empty = Def_val_empty
   ; def_val_dec = (fun e -> Def_val_dec e)
   ; def_val_aux = (fun (defval,aux) -> Def_val_aux (defval,aux))
@@ -742,8 +733,12 @@ let compute_exp_alg bot join =
   ; e_vector_append = (fun ((v1,e1),(v2,e2)) -> (join v1 v2, E_vector_append (e1,e2)))
   ; e_list = split_join (fun es -> E_list es)
   ; e_cons = (fun ((v1,e1),(v2,e2)) -> (join v1 v2, E_cons (e1,e2)))
-  ; e_record = (fun (vs,fexps) -> (vs, E_record fexps))
-  ; e_record_update = (fun ((v1,e1),(vf,fexp)) -> (join v1 vf, E_record_update (e1,fexp)))
+  ; e_record = (fun fexps ->
+    let vs, fexps = List.split fexps in
+    (join_list vs, E_record fexps))
+  ; e_record_update = (fun ((v1,e1),fexps) ->
+    let (vps,fexps) = List.split fexps in
+    (join_list (v1::vps), E_record_update (e1,fexps)))
   ; e_field = (fun ((v1,e1),id) -> (v1, E_field (e1,id)))
   ; e_case = (fun ((v1,e1),pexps) ->
     let (vps,pexps) = List.split pexps in
@@ -783,10 +778,6 @@ let compute_exp_alg bot join =
   ; lEXP_aux = (fun ((vl,lexp),annot) -> (vl, LEXP_aux (lexp,annot)))
   ; fE_Fexp = (fun (id,(v,e)) -> (v, FE_Fexp (id,e)))
   ; fE_aux = (fun ((vf,fexp),annot) -> (vf, FE_aux (fexp,annot)))
-  ; fES_Fexps = (fun (fexps,b) ->
-    let (vs,fexps) = List.split fexps in
-    (join_list vs, FES_Fexps (fexps,b)))
-  ; fES_aux = (fun ((vf,fexp),annot) -> (vf, FES_aux (fexp,annot)))
   ; def_val_empty = (bot, Def_val_empty)
   ; def_val_dec = (fun (v,e) -> (v, Def_val_dec e))
   ; def_val_aux = (fun ((v,defval),aux) -> (v, Def_val_aux (defval,aux)))
@@ -843,8 +834,8 @@ let pure_exp_alg bot join =
   ; e_vector_append = (fun (v1,v2) -> join v1 v2)
   ; e_list = join_list
   ; e_cons = (fun (v1,v2) -> join v1 v2)
-  ; e_record = (fun vs -> vs)
-  ; e_record_update = (fun (v1,vf) -> join v1 vf)
+  ; e_record = (fun vs -> join_list vs)
+  ; e_record_update = (fun (v1,vf) -> join_list (v1::vf))
   ; e_field = (fun (v1,id) -> v1)
   ; e_case = (fun (v1,vps) -> join_list (v1::vps))
   ; e_try = (fun (v1,vps) -> join_list (v1::vps))
@@ -873,8 +864,6 @@ let pure_exp_alg bot join =
   ; lEXP_aux = (fun (vl,annot) -> vl)
   ; fE_Fexp = (fun (id,v) -> v)
   ; fE_aux = (fun (vf,annot) -> vf)
-  ; fES_Fexps = (fun (vs,b) -> join_list vs)
-  ; fES_aux = (fun (vf,annot) -> vf)
   ; def_val_empty = bot
   ; def_val_dec = (fun v -> v)
   ; def_val_aux = (fun (v,aux) -> v)
diff --git a/src/rewriter.mli b/src/rewriter.mli
index 15e704df..9da94a99 100644
--- a/src/rewriter.mli
+++ b/src/rewriter.mli
@@ -107,7 +107,7 @@ type ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg =
 (* fold over pat_aux expressions *)
 
 (* the type of interpretations of expressions *)
-type ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_aux,
+type ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,
       'opt_default_aux,'opt_default,'pexp,'pexp_aux,'letbind_aux,'letbind,
       'pat,'pat_aux,'fpat,'fpat_aux) exp_alg = 
  { e_block                  : 'exp list -> 'exp_aux
@@ -130,8 +130,8 @@ type ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_aux,
  ; e_vector_append          : 'exp * 'exp -> 'exp_aux
  ; e_list                   : 'exp list -> 'exp_aux
  ; e_cons                   : 'exp * 'exp -> 'exp_aux
- ; e_record                 : 'fexps -> 'exp_aux
- ; e_record_update          : 'exp * 'fexps -> 'exp_aux
+ ; e_record                 : 'fexp list -> 'exp_aux
+ ; e_record_update          : 'exp * 'fexp list -> 'exp_aux
  ; e_field                  : 'exp * id -> 'exp_aux
  ; e_case                   : 'exp * 'pexp list -> 'exp_aux
  ; e_try                    : 'exp * 'pexp list -> 'exp_aux
@@ -160,8 +160,6 @@ type ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_aux,
  ; lEXP_aux                 : 'lexp_aux * 'a annot -> 'lexp
  ; fE_Fexp                  : id * 'exp -> 'fexp_aux
  ; fE_aux                   : 'fexp_aux * 'a annot -> 'fexp
- ; fES_Fexps                : 'fexp list * bool -> 'fexps_aux
- ; fES_aux                  : 'fexps_aux * 'a annot -> 'fexps
  ; def_val_empty            : 'opt_default_aux
  ; def_val_dec              : 'exp -> 'opt_default_aux
  ; def_val_aux              : 'opt_default_aux * 'a annot -> 'opt_default
@@ -177,34 +175,34 @@ type ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_aux,
 val fold_pat : ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg -> 'a pat -> 'pat
 
 (* fold over expressions *)
-val fold_exp : ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_aux,
+val fold_exp : ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,
       'opt_default_aux,'opt_default,'pexp,'pexp_aux,'letbind_aux,'letbind,
       'pat,'pat_aux,'fpat,'fpat_aux) exp_alg -> 'a exp -> 'exp
 
-val fold_letbind : ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_aux,
+val fold_letbind : ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,
       'opt_default_aux,'opt_default,'pexp,'pexp_aux,'letbind_aux,'letbind,
       'pat,'pat_aux,'fpat,'fpat_aux) exp_alg -> 'a letbind -> 'letbind
 
-val fold_pexp : ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_aux,
+val fold_pexp : ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,
       'opt_default_aux,'opt_default,'pexp,'pexp_aux,'letbind_aux,'letbind,
       'pat,'pat_aux,'fpat,'fpat_aux) exp_alg -> 'a pexp -> 'pexp
 
-val fold_pexp : ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_aux,
+val fold_pexp : ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,
       'opt_default_aux,'opt_default,'pexp,'pexp_aux,'letbind_aux,'letbind,
       'pat,'pat_aux,'fpat,'fpat_aux) exp_alg -> 'a pexp -> 'pexp
 
-val fold_funcl : ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_aux,
+val fold_funcl : ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,
       'opt_default_aux,'opt_default,'a pexp,'pexp_aux,'letbind_aux,'letbind,
       'pat,'pat_aux,'fpat,'fpat_aux) exp_alg -> 'a funcl -> 'a funcl
 
-val fold_function : ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_aux,
+val fold_function : ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,
       'opt_default_aux,'opt_default, 'a pexp,'pexp_aux,'letbind_aux,'letbind,
       'pat,'pat_aux,'fpat,'fpat_aux) exp_alg -> 'a fundef -> 'a fundef
 
 val id_pat_alg : ('a,'a pat, 'a pat_aux, 'a fpat, 'a fpat_aux) pat_alg
 val id_exp_alg :
   ('a,'a exp,'a exp_aux,'a lexp,'a lexp_aux,'a fexp,
-  'a fexp_aux,'a fexps,'a fexps_aux,
+  'a fexp_aux,
   'a opt_default_aux,'a opt_default,'a pexp,'a pexp_aux,
   'a letbind_aux,'a letbind,
   'a pat,'a pat_aux,'a fpat,'a fpat_aux) exp_alg
@@ -214,7 +212,7 @@ val compute_pat_alg : 'b -> ('b -> 'b -> 'b) ->
 
 val compute_exp_alg : 'b -> ('b -> 'b -> 'b) ->
   ('a,('b * 'a exp),('b * 'a exp_aux),('b * 'a lexp),('b * 'a lexp_aux),('b * 'a fexp),
-  ('b * 'a fexp_aux),('b * 'a fexps),('b * 'a fexps_aux),
+  ('b * 'a fexp_aux),
   ('b * 'a opt_default_aux),('b * 'a opt_default),('b * 'a pexp),('b * 'a pexp_aux),
   ('b * 'a letbind_aux),('b * 'a letbind),
   ('b * 'a pat),('b * 'a pat_aux),('b * 'a fpat),('b * 'a fpat_aux)) exp_alg
@@ -224,7 +222,7 @@ val pure_pat_alg : 'b -> ('b -> 'b -> 'b) -> ('a,'b,'b,'b,'b) pat_alg
 val pure_exp_alg : 'b -> ('b -> 'b -> 'b) ->
   ('a,'b,'b,'b,'b,'b,
   'b,'b,'b,
-  'b,'b,'b,'b,
+  'b,'b,
   'b,'b,
   'b,'b,'b,'b) exp_alg
 
@@ -248,6 +246,4 @@ val fix_eff_pexp : tannot pexp -> tannot pexp
 
 val fix_eff_fexp : tannot fexp -> tannot fexp
 
-val fix_eff_fexps : tannot fexps -> tannot fexps
-
 val fix_eff_opt_default : tannot opt_default -> tannot opt_default
diff --git a/src/rewrites.ml b/src/rewrites.ml
index 2734e91f..8c1311a0 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -513,8 +513,8 @@ let rewrite_sizeof (Defs defs) =
     ; e_vector_append = (fun ((e1,e1'),(e2,e2')) -> (E_vector_append (e1,e2), E_vector_append (e1',e2')))
     ; e_list = (fun es -> let (es, es') = List.split es in (E_list es, E_list es'))
     ; e_cons = (fun ((e1,e1'),(e2,e2')) -> (E_cons (e1,e2), E_cons (e1',e2')))
-    ; e_record = (fun (fexps, fexps') -> (E_record fexps, E_record fexps'))
-    ; e_record_update = (fun ((e1,e1'),(fexp,fexp')) -> (E_record_update (e1,fexp), E_record_update (e1',fexp')))
+    ; e_record = (fun fexps -> let (fexps, fexps') = List.split fexps in (E_record fexps, E_record fexps'))
+    ; e_record_update = (fun ((e1,e1'),fexps) -> let (fexps, fexps') = List.split fexps in (E_record_update (e1,fexps), E_record_update (e1',fexps')))
     ; e_field = (fun ((e1,e1'),id) -> (E_field (e1,id), E_field (e1',id)))
     ; e_case = (fun ((e1,e1'),pexps) -> let (pexps, pexps') = List.split pexps in (E_case (e1,pexps), E_case (e1',pexps')))
     ; e_try = (fun ((e1,e1'),pexps) -> let (pexps, pexps') = List.split pexps in (E_try (e1,pexps), E_try (e1',pexps')))
@@ -543,8 +543,6 @@ let rewrite_sizeof (Defs defs) =
     ; lEXP_aux = (fun ((lexp,lexp'),annot) -> (LEXP_aux (lexp,annot), LEXP_aux (lexp',annot)))
     ; fE_Fexp = (fun (id,(e,e')) -> (FE_Fexp (id,e), FE_Fexp (id,e')))
     ; fE_aux = (fun ((fexp,fexp'),annot) -> (FE_aux (fexp,annot), FE_aux (fexp',annot)))
-    ; fES_Fexps = (fun (fexps,b) -> let (fexps, fexps') = List.split fexps in (FES_Fexps (fexps,b), FES_Fexps (fexps',b)))
-    ; fES_aux = (fun ((fexp,fexp'),annot) -> (FES_aux (fexp,annot), FES_aux (fexp',annot)))
     ; def_val_empty = (Def_val_empty, Def_val_empty)
     ; def_val_dec = (fun (e,e') -> (Def_val_dec e, Def_val_dec e'))
     ; def_val_aux = (fun ((defval,defval'),aux) -> (Def_val_aux (defval,aux), Def_val_aux (defval',aux)))
@@ -1173,7 +1171,7 @@ let rec pat_to_exp ((P_aux (pat,(l,annot))) as p_aux) =
   | P_id id -> rewrap (E_id id)
   | P_app (id,pats) -> rewrap (E_app (id, List.map pat_to_exp pats))
   | P_record (fpats,b) ->
-      rewrap (E_record (FES_aux (FES_Fexps (List.map fpat_to_fexp fpats,b),(l,annot))))
+      rewrap (E_record (List.map fpat_to_fexp fpats))
   | P_vector pats -> rewrap (E_vector (List.map pat_to_exp pats))
   | P_vector_concat pats -> begin
       let empty_vec = E_aux (E_vector [], (l,())) in
@@ -1728,8 +1726,8 @@ let rec rewrite_lexp_to_rhs ((LEXP_aux(lexp,((l,_) as annot))) as le) =
        let env = env_of_annot lannot in
        match Env.expand_synonyms env (typ_of_annot lannot) with
        | Typ_aux (Typ_id rectyp_id, _) | Typ_aux (Typ_app (rectyp_id, _), _) when Env.is_record rectyp_id env ->
-          let field_update exp = FES_aux (FES_Fexps ([FE_aux (FE_Fexp (id, exp), annot)], false), annot) in
-          (lhs, (fun exp -> rhs (E_aux (E_record_update (lexp_to_exp lexp, field_update exp), lannot))))
+          let field_update exp = FE_aux (FE_Fexp (id, exp), annot) in
+          (lhs, (fun exp -> rhs (E_aux (E_record_update (lexp_to_exp lexp, [field_update exp]), lannot))))
        | _ -> raise (Reporting.err_unreachable l __POS__ ("Unsupported lexp: " ^ string_of_lexp le))
      end
   | _ -> raise (Reporting.err_unreachable l __POS__ ("Unsupported lexp: " ^ string_of_lexp le))
@@ -2590,7 +2588,7 @@ let rewrite_defs_letbind_effects =
   and value_optdefault (Def_val_aux (o,_)) = match o with
     | Def_val_empty -> true
     | Def_val_dec e -> value e
-  and value_fexps (FES_aux (FES_Fexps (fexps,_),_)) =
+  and value_fexps fexps =
     List.fold_left (fun b (FE_aux (FE_Fexp (_,e),_)) -> b && value e) true fexps in
 
 
@@ -2621,11 +2619,6 @@ let rewrite_defs_letbind_effects =
   and n_pexpL (newreturn : bool) (pexps : 'a pexp list) (k : 'a pexp list -> 'a exp) : 'a exp =
     mapCont (n_pexp newreturn) pexps k
 
-  and n_fexps (fexps : 'a fexps) (k : 'a fexps -> 'a exp) : 'a exp = 
-    let (FES_aux (FES_Fexps (fexps_aux,b),annot)) = fexps in
-    n_fexpL fexps_aux (fun fexps_aux -> 
-    k (fix_eff_fexps (FES_aux (FES_Fexps (fexps_aux,b),annot))))
-
   and n_opt_default (opt_default : 'a opt_default) (k : 'a opt_default -> 'a exp) : 'a exp = 
     let (Def_val_aux (opt_default,annot)) = opt_default in
     match opt_default with
@@ -2774,11 +2767,11 @@ let rewrite_defs_letbind_effects =
        n_exp_name exp2 (fun exp2 ->
        k (rewrap (E_cons (exp1,exp2)))))
     | E_record fexps ->
-       n_fexps fexps (fun fexps ->
+       n_fexpL fexps (fun fexps ->
        k (rewrap (E_record fexps)))
     | E_record_update (exp1,fexps) ->
        n_exp_name exp1 (fun exp1 ->
-       n_fexps fexps (fun fexps ->
+       n_fexpL fexps (fun fexps ->
        k (rewrap (E_record_update (exp1,fexps)))))
     | E_field (exp1,id) ->
        n_exp_name exp1 (fun exp1 ->
@@ -4155,7 +4148,7 @@ and fexps_of_mfpats mfpats flag annot =
   let fexp_of_mfpat (MFP_aux (MFP_mpat (id, mpat), annot)) =
     FE_aux (FE_Fexp (id, exp_of_mpat mpat), annot)
   in
-  FES_aux (FES_Fexps (List.map fexp_of_mfpat mfpats, flag), annot)
+  List.map fexp_of_mfpat mfpats
 
 and pat_of_mpat (MP_aux (mpat, annot)) =
   match mpat with
diff --git a/src/spec_analysis.ml b/src/spec_analysis.ml
index fa68c6f2..180b96b2 100644
--- a/src/spec_analysis.ml
+++ b/src/spec_analysis.ml
@@ -210,11 +210,11 @@ let rec fv_of_exp consider_var bound used set (E_aux (e,(_,tannot))) : (Nameset.
   | E_vector_update(v,i,e) -> list_fv bound used set [v;i;e]
   | E_vector_update_subrange(v,i1,i2,e) -> list_fv bound used set [v;i1;i2;e]
   | E_vector_append(e1,e2) | E_cons(e1,e2) -> list_fv bound used set [e1;e2]
-  | E_record (FES_aux(FES_Fexps(fexps,_),_)) ->
+  | E_record fexps ->
      let used = Nameset.union (free_type_names_tannot consider_var tannot) used in
      List.fold_right
        (fun (FE_aux(FE_Fexp(_,e),_)) (b,u,s) -> fv_of_exp consider_var b u s e) fexps (bound,used,set)
-  | E_record_update(e,(FES_aux(FES_Fexps(fexps,_),_))) ->
+  | E_record_update(e, fexps) ->
     let b,u,s = fv_of_exp consider_var bound used set e in
     List.fold_right
       (fun (FE_aux(FE_Fexp(_,e),_)) (b,u,s) -> fv_of_exp consider_var b u s e) fexps (b,u,s)
diff --git a/src/type_check.ml b/src/type_check.ml
index d39ce27d..435c5cd8 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -2293,7 +2293,7 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ
           annot_exp (E_list checked_xs) typ
        | None -> typ_error l ("List " ^ string_of_exp exp ^ " must have list type, got " ^ string_of_typ typ)
      end
-  | E_record_update (exp, FES_aux (FES_Fexps (fexps, flag), (l, ()))), _ ->
+  | E_record_update (exp, fexps), _ ->
      (* TODO: this could also infer exp - also fix code duplication with E_record below *)
      let checked_exp = crule check_exp env exp typ in
      let rectyp_id = match Env.expand_synonyms env typ with
@@ -2308,8 +2308,8 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ
        let checked_exp = crule check_exp env exp field_typ' in
        FE_aux (FE_Fexp (field, checked_exp), (l, None))
      in
-     annot_exp (E_record_update (checked_exp, FES_aux (FES_Fexps (List.map check_fexp fexps, flag), (l, None)))) typ
-  | E_record (FES_aux (FES_Fexps (fexps, flag), (l, ()))), _ ->
+     annot_exp (E_record_update (checked_exp, List.map check_fexp fexps)) typ
+  | E_record fexps, _ ->
      (* TODO: check record fields are total *)
      let rectyp_id = match Env.expand_synonyms env typ with
        | Typ_aux (Typ_id rectyp_id, _) | Typ_aux (Typ_app (rectyp_id, _), _) when Env.is_record rectyp_id env ->
@@ -2323,7 +2323,7 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ
        let checked_exp = crule check_exp env exp field_typ' in
        FE_aux (FE_Fexp (field, checked_exp), (l, None))
      in
-     annot_exp (E_record (FES_aux (FES_Fexps (List.map check_fexp fexps, flag), (l, None)))) typ
+     annot_exp (E_record (List.map check_fexp fexps)) typ
   | E_let (LB_aux (letbind, (let_loc, _)), exp), _ ->
      begin
        match letbind with
@@ -3165,7 +3165,7 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) =
      annot_exp (E_tuple inferred_exps) (mk_typ (Typ_tup (List.map typ_of inferred_exps)))
   | E_assign (lexp, bind) ->
      fst (bind_assignment env lexp bind)
-  | E_record_update (exp, FES_aux (FES_Fexps (fexps, flag), (l, ()))) ->
+  | E_record_update (exp, fexps) ->
      let inferred_exp = irule infer_exp env exp in
      let typ = typ_of inferred_exp in
      let rectyp_id = match Env.expand_synonyms env typ with
@@ -3180,7 +3180,7 @@ and infer_exp env (E_aux (exp_aux, (l, ())) as exp) =
        let inferred_exp = crule check_exp env exp field_typ' in
        FE_aux (FE_Fexp (field, inferred_exp), (l, None))
      in
-     annot_exp (E_record_update (inferred_exp, FES_aux (FES_Fexps (List.map check_fexp fexps, flag), (l, None)))) typ
+     annot_exp (E_record_update (inferred_exp, List.map check_fexp fexps)) typ
   | E_cast (typ, exp) ->
      let checked_exp = crule check_exp env exp typ in
      annot_exp (E_cast (typ, checked_exp)) typ
@@ -3857,14 +3857,14 @@ and propagate_exp_effect_aux = function
      let p_cases = List.map propagate_pexp_effect cases in
      let case_eff = List.fold_left union_effects no_effect (List.map snd p_cases) in
      E_case (p_exp, List.map fst p_cases), union_effects (effect_of p_exp) case_eff
-  | E_record_update (exp, FES_aux (FES_Fexps (fexps, flag), (l, _))) ->
+  | E_record_update (exp, fexps) ->
      let p_exp = propagate_exp_effect exp in
      let p_fexps = List.map propagate_fexp_effect fexps in
-     E_record_update (p_exp, FES_aux (FES_Fexps (List.map fst p_fexps, flag), (l, None))),
+     E_record_update (p_exp, List.map fst p_fexps),
      List.fold_left union_effects no_effect (effect_of p_exp :: List.map snd p_fexps)
-  | E_record (FES_aux (FES_Fexps (fexps, flag), (l, _))) ->
+  | E_record fexps ->
      let p_fexps = List.map propagate_fexp_effect fexps in
-     E_record (FES_aux (FES_Fexps (List.map fst p_fexps, flag), (l, None))),
+     E_record (List.map fst p_fexps),
      List.fold_left union_effects no_effect (List.map snd p_fexps)
   | E_try (exp, cases) ->
      let p_exp = propagate_exp_effect exp in