let rec pp p fmt = 
    function
      | Apply, al -> 
          let op = Format.sprintf "apply" in 
            Pretty.string fmt "(";
            Pretty.infixl p " $ " fmt al;
            Pretty.string fmt ")"
      | S, [] -> 
          Pretty.string fmt "S"
      | K, [] ->
          Pretty.string fmt "K"
      | I, [] ->
          Pretty.string fmt "I"
      | C, [] ->
          Pretty.string fmt "C"
      | Reify(f, _), [] ->
          let str = Format.sprintf "'%s'" (to_string f) in
            Pretty.string fmt str
      | _ ->
          invalid_arg "Ill-formed application in theory of functions"

  and to_string (sym, _) = 
    match sym with
      | Uninterp(op) -> Uninterp.to_string op
      | Arith(op) -> Arith.to_string op
      | Product(op) -> Product.to_string op
      | Bv(op) -> Bv.to_string op
      | Coproduct(op) -> Coproduct.to_string op
      | Arrays(op) -> Array.to_string op
      | Pp(op) -> Pprod.to_string op
      | Propset(op) -> Propset.to_string op
      | Cl(op) -> invalid_arg "Reified combinatory logic symbol"