1.1 --- a/test/Tools/isac/Test_Isac.thy	Fri Apr 24 09:01:48 2020 +0200
     1.2 +++ b/test/Tools/isac/Test_Isac.thy	Mon Apr 27 12:36:21 2020 +0200
     1.3 @@ -100,7 +100,7 @@
     1.4    open Error_Pattern;
     1.5    open Error_Pattern_Def;
     1.6    open In_Chead;
     1.7 -  open Rtools;                 .trtas2str;
     1.8 +  open Rtools;
     1.9    open Chead;                  pt_extract;
    1.10    open Generate;               (* NONE *)
    1.11    open Ctree;                  append_problem;
    1.12 @@ -126,7 +126,7 @@
    1.13    open Rewrite;
    1.14    open Eval;                   get_pair;
    1.15    open TermC;                  atomt;
    1.16 -  open Celem;                  e_pbt;
    1.17 +  open Celem;
    1.18    open Rule;
    1.19    open Rule_Set;               Sequence;
    1.20    open Exec_Def
    1.21 @@ -188,8 +188,10 @@
    1.22    ML_file "BaseDefinitions/error-fill-def.sml"
    1.23    ML_file "BaseDefinitions/rule-set.sml"
    1.24    ML_file "BaseDefinitions/check-unique.sml"
    1.25 +(*called by Know_Store*)
    1.26    ML_file "BaseDefinitions/calcelems.sml"
    1.27    ML_file "BaseDefinitions/termC.sml"
    1.28 +  ML_file substitution.sml
    1.29    ML_file "BaseDefinitions/contextC.sml"
    1.30    ML_file "BaseDefinitions/environment.sml"
    1.31    ML_file "BaseDefinitions/kestore.sml"    (* setup in ADDTEST/accumulate-val/lucas_interpreter.sml*)