let rec atom_globs a acc = match a with | Atom.True | Atom.False -> acc | Atom.Comp (t1, _, t2) -> term_globs t1 (term_globs t2 acc) | Atom.Ite (sa, a1, a2) -> Term.Set.union (satom_globs sa) (atom_globs a1 (atom_globs a2 acc)) and satom_globs sa = SAtom.fold atom_globs sa Term.Set.empty