added print_pterm_fun, which is a function that is like print_pterm but returns a string. For use in the Python interface
Authored by: "kifer" 2018-06-22
Parent: [r9376]
Child: [r9378]
