1.1 --- a/test/Tools/isac/Test_Isac.thy	Sun Apr 19 16:43:53 2020 +0200
     1.2 +++ b/test/Tools/isac/Test_Isac.thy	Mon Apr 20 15:54:19 2020 +0200
     1.3 @@ -123,12 +123,12 @@
     1.4    open ContextC;               transfer_asms_from_to;
     1.5    open Tactic;                 (* NONE *)
     1.6    open Model;                  (* NONE *)
     1.7 -  open Rewrite;                mk_thm;
     1.8 +  open Rewrite;
     1.9    open Eval;                   get_pair;
    1.10    open TermC;                  atomt;
    1.11    open Celem;                  e_pbt;
    1.12    open Rule;
    1.13 -  open Rule_Set
    1.14 +  open Rule_Set;               Sequence;
    1.15    open Exec_Def
    1.16    open ThyC
    1.17    open ThmC_Def
    1.18 @@ -187,6 +187,7 @@
    1.19    ML_file "BaseDefinitions/thmC-def.sml"
    1.20    ML_file "BaseDefinitions/error-fill-def.sml"
    1.21    ML_file "BaseDefinitions/rule-set.sml"
    1.22 +  ML_file "BaseDefinitions/check-unique.sml"
    1.23    ML_file "BaseDefinitions/calcelems.sml"
    1.24    ML_file "BaseDefinitions/termC.sml"
    1.25    ML_file "BaseDefinitions/contextC.sml"
    1.26 @@ -248,7 +249,7 @@
    1.27    ML_file "Interpret/istate.sml"
    1.28    ML_file "Interpret/sub-problem.sml"
    1.29    ML_file "Interpret/rewtools.sml"
    1.30 -  ML_file "Interpret/error-pattern.sml"
    1.31 +  ML_file "Interpret/error-fill-pattern.sml"
    1.32    ML_file "Interpret/li-tool.sml"
    1.33    ML_file "Interpret/lucas-interpreter.sml"
    1.34    ML_file "Interpret/step-solve.sml"