1.1 --- a/test/Tools/isac/Test_Isac.thy	Thu Sep 23 12:56:51 2010 +0200
     1.2 +++ b/test/Tools/isac/Test_Isac.thy	Thu Sep 23 14:49:23 2010 +0200
     1.3 @@ -81,12 +81,10 @@
     1.4  ML {*print_depth 99*}
     1.5  
     1.6  ML {*
     1.7 -fun term2str trm = Print_Mode.setmp (Print_Mode.input ::
     1.8 -        filter (curry (op =) Symbol.xsymbolsN) (print_mode_value ()))
     1.9 -        (Syntax.string_of_term @{context}) trm;
    1.10 -val trm = str2term "a+b"; term2str trm;
    1.11 -val trm = str2term "x ^^^ 2 * c + c_2 = x ^^^ 2 * c + c_2 + c_3"; term2str trm;
    1.12 -"=========================================================";
    1.13 +str2term "a + b";
    1.14 +str2term "a - b";
    1.15 +str2term "a * b";
    1.16 +str2term "a / b";
    1.17  *}
    1.18  
    1.19  use "Knowledge/integrate.sml";