diff --git a/sledge/src/llair/exp.ml b/sledge/src/llair/exp.ml
index 261baff1d..c9c01dc5e 100644
--- a/sledge/src/llair/exp.ml
+++ b/sledge/src/llair/exp.ml
@@ -1326,13 +1326,13 @@ let map e ~f =
   in
   fix map_ (fun e -> e) e
 
-let rename e sub =
-  let rec rename_ e sub =
+let rename sub e =
+  let rec rename_ sub e =
     match e with
     | Var _ -> Var.Subst.apply sub e
-    | _ -> map ~f:(fun f -> rename_ f sub) e
+    | _ -> map ~f:(rename_ sub) e
   in
-  rename_ e sub |> check (invariant ~partial:true)
+  rename_ sub e |> check (invariant ~partial:true)
 
 (** Query *)
 
diff --git a/sledge/src/llair/exp.mli b/sledge/src/llair/exp.mli
index 416e23c2c..f8070f81b 100644
--- a/sledge/src/llair/exp.mli
+++ b/sledge/src/llair/exp.mli
@@ -208,7 +208,7 @@ val fold : t -> init:'a -> f:(t -> 'a -> 'a) -> 'a
 (** Transform *)
 
 val map : t -> f:(t -> t) -> t
-val rename : t -> Var.Subst.t -> t
+val rename : Var.Subst.t -> t -> t
 
 (** Query *)
 
diff --git a/sledge/src/symbheap/equality.ml b/sledge/src/symbheap/equality.ml
index 36d920e47..1837d9231 100644
--- a/sledge/src/symbheap/equality.ml
+++ b/sledge/src/symbheap/equality.ml
@@ -285,7 +285,7 @@ let map_exps ({sat= _; rep} as r) ~f =
     pf "%a" pp_diff (r, r') ;
     invariant r']
 
-let rename r sub = map_exps r ~f:(fun e -> Exp.rename e sub)
+let rename r sub = map_exps r ~f:(Exp.rename sub)
 
 let fold_exps r ~init ~f =
   Map.fold r.rep ~f:(fun ~key ~data z -> f (f z data) key) ~init
diff --git a/sledge/src/symbheap/sh.ml b/sledge/src/symbheap/sh.ml
index a733226a8..06f0659e6 100644
--- a/sledge/src/symbheap/sh.ml
+++ b/sledge/src/symbheap/sh.ml
@@ -186,11 +186,11 @@ let rec simplify {us; xs; cong; pure; heap; djns} =
 (** Quantification and Vocabulary *)
 
 let rename_seg sub ({loc; bas; len; siz; arr} as h) =
-  let loc = Exp.rename loc sub in
-  let bas = Exp.rename bas sub in
-  let len = Exp.rename len sub in
-  let siz = Exp.rename siz sub in
-  let arr = Exp.rename arr sub in
+  let loc = Exp.rename sub loc in
+  let bas = Exp.rename sub bas in
+  let len = Exp.rename sub len in
+  let siz = Exp.rename sub siz in
+  let arr = Exp.rename sub arr in
   ( if
     loc == h.loc && bas == h.bas && len == h.len && siz == h.siz
     && arr == h.arr
@@ -203,9 +203,7 @@ let rename_seg sub ({loc; bas; len; siz; arr} as h) =
     invariant *)
 let rec apply_subst sub ({us= _; xs= _; cong; pure; heap; djns} as q) =
   let cong = Equality.rename cong sub in
-  let pure =
-    List.map_preserving_phys_equal pure ~f:(fun b -> Exp.rename b sub)
-  in
+  let pure = List.map_preserving_phys_equal pure ~f:(Exp.rename sub) in
   let heap = List.map_preserving_phys_equal heap ~f:(rename_seg sub) in
   let djns =
     List.map_preserving_phys_equal djns ~f:(fun d ->
diff --git a/sledge/src/symbheap/state_domain.ml b/sledge/src/symbheap/state_domain.ml
index 3c1ad8ea9..174f7c3ed 100644
--- a/sledge/src/symbheap/state_domain.ml
+++ b/sledge/src/symbheap/state_domain.ml
@@ -82,7 +82,7 @@ let jump actuals formals ?temps q =
   ;
   let q', freshen_locals = Sh.freshen q ~wrt:(Var.Set.of_list formals) in
   let and_eq q formal actual =
-    let actual' = Exp.rename actual freshen_locals in
+    let actual' = Exp.rename freshen_locals actual in
     Sh.and_ (Exp.eq (Exp.var formal) actual') q
   in
   let and_eqs formals actuals q =
@@ -108,7 +108,7 @@ let call ~summaries actuals formals locals globals q =
   let wrt = Set.add_list formals locals in
   let q', freshen_locals = Sh.freshen q ~wrt in
   let and_eq q formal actual =
-    let actual' = Exp.rename actual freshen_locals in
+    let actual' = Exp.rename freshen_locals actual in
     Sh.and_ (Exp.eq (Exp.var formal) actual') q
   in
   let and_eqs formals actuals q =
@@ -190,7 +190,7 @@ let create_summary ~locals ~formals ~entry ~current =
   let restore_formals q =
     Set.fold formals ~init:q ~f:(fun q var ->
         let var = Exp.var var in
-        let renamed_var = Exp.rename var subst in
+        let renamed_var = Exp.rename subst var in
         Sh.and_ (Exp.eq renamed_var var) q )
   in
   (* Add back the original formals name *)