1.1 --- a/src/Tools/isac/Build_Isac.thy	Sun Apr 19 11:07:02 2020 +0200
     1.2 +++ b/src/Tools/isac/Build_Isac.thy	Sun Apr 19 12:22:37 2020 +0200
     1.3 @@ -13,7 +13,7 @@
     1.4  
     1.5  theory Build_Isac 
     1.6  imports
     1.7 -(*  theory KEStore imports Complex_Main
     1.8 +(*  theory Know_Store imports Complex_Main
     1.9        ML_file libraryC.sml
    1.10        ML_file theoryC.sml
    1.11        ML_file unparseC.sml                                                                                                  
    1.12 @@ -25,7 +25,7 @@
    1.13        ML_file "error-fill-def.sml"
    1.14        ML_file "rule-set.sml"
    1.15        ML_file calcelems.sml
    1.16 -  theory BaseDefinitions imports KEStore
    1.17 +  theory BaseDefinitions imports Know_Store
    1.18      ML_file termC.sml
    1.19      ML_file contextC.sml
    1.20      ML_file environment.sml
    1.21 @@ -147,7 +147,7 @@
    1.22  \<close>
    1.23  subsection \<open>(0) Survey on remaining Unsynchronized.ref\<close>
    1.24  text \<open>
    1.25 -  REPLACE BY KEStore... (has been overlooked)
    1.26 +  REPLACE BY Know_Store... (has been overlooked)
    1.27      calcelems.sml:val rew_ord' = Unsynchronized.ref ...
    1.28    KEEP FOR TRACING
    1.29      calcelems.sml:val trace_rewrite = Unsynchronized.ref false;