Added [disjoint].

src/Toolbox.cppo.ml

@@ -144,15 +144,24 @@ end
 let ba : nominal_term -> Atom.Set.t =
   new ba # visit_term ()
 
+let ba_list ts =
+  List.fold_left
+    (fun accu t -> Atom.Set.disjoint_union accu (ba t))
+    Atom.Set.empty ts
+
 (* [wf t] checks whether the term [t] is well-formed, and returns no result.
    The exception [IllFormed x] is raised if the atom [x] occurs twice in a
-   binding position.*)
+   binding position. *)
 
 let wf t =
   let (_ : Atom.Set.t) = ba t in ()
 
-(* TEMPORARY add a disjointness check; this boils down to checking that a
-   list of terms is well-formed. *)
+(* [disjoint ts] checks that the terms in the list [ts] are well-formed and
+   disjoint. The exception [IllFormed x] is raised if the atom [x] occurs
+   twice in a binding position. *)
+
+let disjoint ts =
+  let (_ : Atom.Set.t) = ba_list ts in ()
 
 (* -------------------------------------------------------------------------- *)