fun term2str trm = Print_Mode.setmp (Print_Mode.input ::

 str2term "a + b";

         filter (curry (op =) Symbol.xsymbolsN) (print_mode_value ()))

 str2term "a - b";

         (Syntax.string_of_term @{context}) trm;

 str2term "a * b";

 val trm = str2term "a+b"; term2str trm;

 str2term "a / b";

 val trm = str2term "x ^^^ 2 * c + c_2 = x ^^^ 2 * c + c_2 + c_3"; term2str trm;

 "=========================================================";