diff --git a/sledge/src/ses/term.ml b/sledge/src/ses/term.ml
index aacccb999..d45b1ac96 100644
--- a/sledge/src/ses/term.ml
+++ b/sledge/src/ses/term.ml
@@ -1035,11 +1035,6 @@ module Var = struct
     | Var _ as v -> Some (v |> check invariant)
     | _ -> None
 
-  let of_reg r =
-    match of_term (of_exp (r : Llair.Reg.t :> Llair.Exp.t)) with
-    | Some v -> v
-    | _ -> violates Llair.Reg.invariant r
-
   let program ~name ~global = Var {name; id= (if global then -1 else 0)}
 
   let fresh name ~wrt =
@@ -1060,9 +1055,6 @@ module Var = struct
     let pp_xs fs xs =
       if not (is_empty xs) then
         Format.fprintf fs "@<2>∃ @[%a@] .@;<1 2>" pp xs
-
-    let of_regs =
-      Llair.Reg.Set.fold ~init:empty ~f:(fun s r -> add s (of_reg r))
   end
 end
 
diff --git a/sledge/src/ses/term.mli b/sledge/src/ses/term.mli
index 64cdc7b3d..662036eff 100644
--- a/sledge/src/ses/term.mli
+++ b/sledge/src/ses/term.mli
@@ -116,7 +116,6 @@ module Var : sig
     val ppx : strength -> t pp
     val pp : t pp
     val pp_xs : t pp
-    val of_regs : Llair.Reg.Set.t -> t
   end
 
   val pp : t pp
@@ -127,7 +126,6 @@ module Var : sig
   val id : t -> int
   val of_ : term -> t
   val of_term : term -> t option
-  val of_reg : Llair.Reg.t -> t
   val program : name:string -> global:bool -> t
   val fresh : string -> wrt:Set.t -> t * Set.t