functor (Seq : Sigs.SEQUENT) (Defs : Sigs.DEFS) ->
  sig
    type seq_t = Seq.t
    type proof_t = Proof.Make(Seq).t
    type defs_t = Defs.t
    type rule_t = Proofrule.Make(Seq).t
    type select_f = int -> proof_t -> int list
    type infrule_app = (seq_t * Tagpairs.t * Tagpairs.t) list * string
    type abdinfrule_f = seq_t -> defs_t -> defs_t list
    type abdbackrule_f = seq_t -> seq_t -> defs_t -> defs_t list
    type abdgenrule_f = seq_t -> defs_t -> (infrule_app * defs_t) list
    type t =
        int -> proof_t -> defs_t -> ((int list * proof_t) * defs_t) Blist.t
    val mk_abdinfrule : abdinfrule_f -> t
    val mk_abdbackrule : select_f -> abdbackrule_f -> t
    val mk_abdgenrule : abdgenrule_f -> t
    val fail : t
    val lift : rule_t -> t
    val compose : t -> t -> t
    val choice : t list -> t
    val attempt : t -> t
    val first : t list -> t
  end