diff --git a/sledge/src/fol.ml b/sledge/src/fol.ml
index 557d18923..935c0d7ec 100644
--- a/sledge/src/fol.ml
+++ b/sledge/src/fol.ml
@@ -1533,6 +1533,10 @@ module Context = struct
     let vs', z = Ses.Equality.and_ (vs_to_ses vs) x y in
     (vs_of_ses vs', z)
 
+  let inter vs x y =
+    let vs', z = Ses.Equality.or_ (vs_to_ses vs) x y in
+    (vs_of_ses vs', z)
+
   let interN vs xs =
     let vs', z = Ses.Equality.orN (vs_to_ses vs) xs in
     (vs_of_ses vs', z)
diff --git a/sledge/src/fol.mli b/sledge/src/fol.mli
index d7982c8b6..ef197b3f1 100644
--- a/sledge/src/fol.mli
+++ b/sledge/src/fol.mli
@@ -205,9 +205,13 @@ module Context : sig
   val union : Var.Set.t -> t -> t -> Var.Set.t * t
   (** Union (that is, conjoin) two contexts of assumptions. *)
 
-  val interN : Var.Set.t -> t list -> Var.Set.t * t
+  val inter : Var.Set.t -> t -> t -> Var.Set.t * t
   (** Intersect (that is, disjoin) contexts of assumptions. *)
 
+  val interN : Var.Set.t -> t list -> Var.Set.t * t
+  (** Intersect contexts of assumptions. Possibly weaker than logical
+      disjunction. *)
+
   val rename : t -> Var.Subst.t -> t
   (** Apply a renaming substitution to the context. *)