1.1 --- a/test/Tools/isac/Test_Isac.thy	Thu Sep 23 08:54:26 2010 +0200
     1.2 +++ b/test/Tools/isac/Test_Isac.thy	Thu Sep 23 12:56:51 2010 +0200
     1.3 @@ -77,9 +77,20 @@
     1.4   	use"complex.sml";
     1.5   	use"diff.sml";
     1.6   	use"diffapp.sml";
     1.7 -(**)
     1.8 -use"Knowledge/integrate.sml";
     1.9 -(**)
    1.10 +*)
    1.11 +ML {*print_depth 99*}
    1.12 +
    1.13 +ML {*
    1.14 +fun term2str trm = Print_Mode.setmp (Print_Mode.input ::
    1.15 +        filter (curry (op =) Symbol.xsymbolsN) (print_mode_value ()))
    1.16 +        (Syntax.string_of_term @{context}) trm;
    1.17 +val trm = str2term "a+b"; term2str trm;
    1.18 +val trm = str2term "x ^^^ 2 * c + c_2 = x ^^^ 2 * c + c_2 + c_3"; term2str trm;
    1.19 +"=========================================================";
    1.20 +*}
    1.21 +
    1.22 +use "Knowledge/integrate.sml";
    1.23 +(*
    1.24  	use"equation.sml";
    1.25  	(*use"inssort.sml"; problems with recdef in Isabelle2002*)
    1.26   	use"logexp.sml";
    1.27 @@ -104,6 +115,9 @@
    1.28  	use"algein.sml";
    1.29   	cd "../..";
    1.30  *)
    1.31 +use_thy "../../Pure/Isar/Test_Parse_Term"
    1.32 +use_thy "../../Pure/Isar/Test_Parsers"
    1.33 +
    1.34  ML{* writeln "**** run tests on IsacKnowledge complete ****************" *};
    1.35  (*
    1.36  val path = "/home/neuper/proto2/testsml2xml/";