let pp p fmt (op, al) =
    let arg = p fmt and str = Pretty.string fmt in
      match (op, al) with
        | Create, [a] ->
            Pretty.apply p fmt ("create", [a])
        | Select, [a; j] -> 
            (match !Pretty.flag with
               | Pretty.Mode.Mixfix -> 
                   arg a; str "["; arg j; str "]"
               | _ -> 
                   Pretty.apply p fmt ("select", [a; j]))
        | Update, [a; i; x] -> 
            (match !Pretty.flag with
               | Pretty.Mode.Mixfix -> 
                   arg a; str "["; arg i; str " := "; arg x; str "]"
               | _ -> 
                   Pretty.apply p fmt ("update", [a; i; x]))
        | _ ->
            invalid_arg "Ill-formed application in theory of arrays"