let rec status = function
  | Var _ -> 
      Variable
  | App(f, al, _) -> 
      let i = Sym.theory_of f in
      let rec loop = function
        | [] ->
            mk_pure(i)
        | a :: al -> 
            (match status a with
               | Variable -> loop al
               | Pure(j) -> 
                   if i = j then loop al else Mixed(j, a)
               | (Mixed _ as m) -> m)
      in
        loop al