1.1 --- a/test/Tools/isac/Test_Isac.thy	Wed Dec 28 11:14:04 2016 +0100
     1.2 +++ b/test/Tools/isac/Test_Isac.thy	Wed Dec 28 13:07:17 2016 +0100
     1.3 @@ -78,8 +78,8 @@
     1.4    open Generate;               (*NONE*)
     1.5    open Ctree;                  append_problem;
     1.6    open Specify;                show_ptyps;
     1.7 -  open Applicable;             (*TODO*)
     1.8 -  open Solve;                  (*TODO*)
     1.9 +  open Applicable;             (*NONE*)
    1.10 +  open Solve;                  (*NONE*)
    1.11  (*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    1.12  *}
    1.13  ML {*
    1.14 @@ -121,7 +121,8 @@
    1.15    ML {*"%%%%%%%%%%%%%%%%% end Minisubpbl.thy %%%%%%%%%%%%%%%%%%%%%%%";*}
    1.16    ML {*"%%%%%%%%%%%%%%%%% start Interpret.thy %%%%%%%%%%%%%%%%%%";*}
    1.17    ML_file "Interpret/mstools.sml"
    1.18 -  ML_file "Interpret/ctree.sml"         (*!...!see(25)*)
    1.19 +  ML_file "Interpret/basic-ctree.sml"   (*!...!see(25)*)
    1.20 +  ML_file "Interpret/ctree.sml" 
    1.21    ML_file "Interpret/ptyps.sml"         (* requires setup from ptyps.thy *)
    1.22    ML {* (*check_unsynchronized_ref (); ==== trick on error: CUT AND PASTE THIS LINE =========*) *}
    1.23  (*TRICK DOESN'T WORK: get_pbt not found: ["IsacKnowledge","Diff","Theorems","diff_sin_chain"]*)