sig
  module type SIG = sig val th : Th.t val f : Sym.t end
  module type TERM =
    sig
      val d_interp : Term.t -> Term.t * Term.t
      val is_interp : Term.t -> bool
      val make : Term.t -> Term.t -> Term.t
      val iterate : Term.t -> int -> Term.t
      val multiplicity : Term.t -> Term.t -> int
      val decompose : Term.t -> (Term.t * int) * Term.t option
      val fold : (Term.t -> int -> '-> 'a) -> Term.t -> '-> 'a
      val iter : (Term.t -> int -> unit) -> Term.t -> unit
      val sigma : Sym.t -> Term.t list -> Term.t
      val map : (Term.t -> Term.t) -> Term.t -> Term.t
    end
  module Make : functor (Sig : SIG-> TERM
end