require symbols to be printable;
to_string and pp functions in module Logic_term.S;
safer renaming, and more consistent constructors (mk_apply x [] == x)