diff --git a/sledge/src/fol.ml b/sledge/src/fol.ml
index 2e2d05f1d..83a38d918 100644
--- a/sledge/src/fol.ml
+++ b/sledge/src/fol.ml
@@ -11,10 +11,11 @@ module Term = struct
   include Ses.Term
 
   let ite = conditional
+  let rename s e = rename (Var.Subst.apply s) e
 end
 
 module Formula = struct
-  include Ses.Term
+  include Term
 
   let inject b = b
   let project e = Some e
@@ -29,6 +30,7 @@ module Context = struct
 
   let and_formula = and_term
   let normalizef = normalize
+  let rename x sub = rename x (Var.Subst.apply sub)
 
   module Subst = struct
     include Subst
diff --git a/sledge/src/ses/equality.mli b/sledge/src/ses/equality.mli
index 16ca6415e..b608a477c 100644
--- a/sledge/src/ses/equality.mli
+++ b/sledge/src/ses/equality.mli
@@ -48,7 +48,7 @@ val or_ : Var.Set.t -> t -> t -> Var.Set.t * t
 val orN : Var.Set.t -> t list -> Var.Set.t * t
 (** Nary disjunction. *)
 
-val rename : t -> Var.Subst.t -> t
+val rename : t -> (Var.t -> Var.t) -> t
 (** Apply a renaming substitution to the relation. *)
 
 val fv : t -> Var.Set.t
diff --git a/sledge/src/ses/term.ml b/sledge/src/ses/term.ml
index f19f45ca3..50952d95c 100644
--- a/sledge/src/ses/term.ml
+++ b/sledge/src/ses/term.ml
@@ -1220,10 +1220,8 @@ let disjuncts e =
   in
   Set.elements (disjuncts_ e)
 
-let rename sub e =
-  map_rec_pre e ~f:(function
-    | Var _ as v -> Some (Var.Subst.apply sub v)
-    | _ -> None )
+let rename f e =
+  map_rec_pre e ~f:(function Var _ as v -> Some (f v) | _ -> None)
 
 (** Traverse *)
 
diff --git a/sledge/src/ses/term.mli b/sledge/src/ses/term.mli
index 445927e47..e2148b072 100644
--- a/sledge/src/ses/term.mli
+++ b/sledge/src/ses/term.mli
@@ -259,7 +259,7 @@ val fold_map_rec_pre :
   t -> init:'a -> f:('a -> t -> ('a * t) option) -> 'a * t
 
 val disjuncts : t -> t list
-val rename : Var.Subst.t -> t -> t
+val rename : (Var.t -> Var.t) -> t -> t
 
 (** Traverse *)