1.1 --- a/src/Tools/isac/Test_Isac.thy	Mon Mar 21 00:32:53 2011 +0100
     1.2 +++ b/src/Tools/isac/Test_Isac.thy	Mon Apr 04 11:05:07 2011 +0200
     1.3 @@ -15,7 +15,12 @@
     1.4  representation of terms and thus break some tests.
     1.5  *)
     1.6  
     1.7 -theory Test_Isac imports "Knowledge/Isac" begin
     1.8 +theory Test_Isac imports
     1.9 +  "Knowledge/Isac"
    1.10 +  "../../../test/Pure/General/Basics"
    1.11 +  "../../../test/Pure/Isar/Test_Parse_Term" (*part.*)
    1.12 +  "../../../test/Pure/Isar/Test_Parsers"
    1.13 +begin
    1.14  
    1.15  ML{* writeln "**** run the tests **************************************" *}
    1.16  ML {* Toplevel.debug := true; *}
    1.17 @@ -42,7 +47,7 @@
    1.18  cd"smltest/Scripts";
    1.19  *)
    1.20  use"../../../test/Tools/isac/ProgLang/termC.sml" (*part.*)
    1.21 -ML {*print_depth 9*}
    1.22 +ML {*print_depth 90*}
    1.23  use"../../../test/Tools/isac/ProgLang/calculate.sml" (*part.*)
    1.24  
    1.25  ML {*store_met*}
    1.26 @@ -55,6 +60,7 @@
    1.27   	cd "../.."; 
    1.28  cd"smltest/ME";
    1.29  *)
    1.30 +
    1.31  use "../../../test/Tools/isac/Interpret/mstools.sml" (*empty*)
    1.32  use "../../../test/Tools/isac/Interpret/ctree.sml"   (*part.*)
    1.33  use "../../../test/Tools/isac/Interpret/ptyps.sml"   (*TODO*)
    1.34 @@ -64,7 +70,7 @@
    1.35          use"solve.sml"; (*detailrls can notyet ackn. 'Rewrite_Set "cancel"' *);
    1.36          use"inform.sml";
    1.37  *)
    1.38 -ML {*print_depth 5*}
    1.39 +ML {*print_depth 300*}
    1.40  use "../../../test/Tools/isac/Interpret/mathengine.sml" (*part.+110310*)
    1.41  ML {**}
    1.42  (*
    1.43 @@ -159,10 +165,6 @@
    1.44  use_thy "../../Tools/isac/ADDTESTS/trace-rewrite/Build_Test"
    1.45  *)
    1.46  use "../../../test/Pure/library.sml" (**)
    1.47 -use_thy "../../../test/Pure/General/Basics"
    1.48 -
    1.49 -use_thy "../../../test/Pure/Isar/Test_Parse_Term" (*part.*)
    1.50 -use_thy "../../../test/Pure/Isar/Test_Parsers"
    1.51  
    1.52  ML{* writeln "**** run tests on IsacKnowledge complete ****************" *}
    1.53  (*