diff --git a/sledge/src/fol/propositional.ml b/sledge/src/fol/propositional.ml
index 35e4656c2..db1519b71 100644
--- a/sledge/src/fol/propositional.ml
+++ b/sledge/src/fol/propositional.ml
@@ -9,7 +9,10 @@
 
 include Propositional_intf
 
-module Make (Trm : TERM) = struct
+module Make (Trm : sig
+  type t [@@deriving compare, equal, sexp]
+end) =
+struct
   (** Sets of formulas *)
   module rec Fmls : (FORMULA_SET with type elt := Fml.t) = struct
     module T = struct
diff --git a/sledge/src/fol/propositional.mli b/sledge/src/fol/propositional.mli
index 948c39a83..f32528117 100644
--- a/sledge/src/fol/propositional.mli
+++ b/sledge/src/fol/propositional.mli
@@ -8,4 +8,10 @@
 (** Propositional formulas *)
 
 include module type of Propositional_intf
-module Make : MAKE
+
+module Make (Trm : sig
+  type t [@@deriving compare, equal, sexp]
+end) : sig
+  module rec Fml : (FORMULA with type trm := Trm.t with type set := Fmls.t)
+  and Fmls : (FORMULA_SET with type elt := Fml.t)
+end
diff --git a/sledge/src/fol/propositional_intf.ml b/sledge/src/fol/propositional_intf.ml
index 4e9d8d9b3..9ebea8fa5 100644
--- a/sledge/src/fol/propositional_intf.ml
+++ b/sledge/src/fol/propositional_intf.ml
@@ -7,10 +7,6 @@
 
 (** Propositional formulas *)
 
-module type TERM = sig
-  type t [@@deriving compare, equal, sexp]
-end
-
 (** Formulas, built from literals with predicate symbols from various
     theories, and propositional constants and connectives. Denote sets of
     structures. *)
@@ -58,8 +54,3 @@ module type FORMULA_SET = sig
 
   val t_of_sexp : Sexp.t -> t
 end
-
-module type MAKE = functor (Trm : TERM) -> sig
-  module rec Fml : (FORMULA with type trm := Trm.t with type set := Fmls.t)
-  and Fmls : (FORMULA_SET with type elt := Fml.t)
-end