1.1 --- a/src/Tools/isac/Knowledge/Build_Thydata.thy	Mon Aug 26 09:20:07 2019 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Build_Thydata.thy	Mon Aug 26 17:40:27 2019 +0200
     1.3 @@ -4,7 +4,7 @@
     1.4  
     1.5  theory Build_Thydata
     1.6  imports 
     1.7 -  Isac "~~/src/Tools/isac/Interpret/Interpret"
     1.8 +  Isac_Knowledge "~~/src/Tools/isac/Interpret/Interpret"
     1.9    Test_Build_Thydata (*for test/../build_thydata.sml, thy_hierarchy.sml*)
    1.10  begin
    1.11  
    1.12 @@ -27,14 +27,14 @@
    1.13    val allthys = Theory.ancestors_of @{theory};
    1.14    val allthys = filter_out (member Context.eq_thy (* thys for isac bootstrap *)
    1.15      [(*@{theory ProgLang}: required in isacthys' below*) @{theory Interpret}, @{theory xmlsrc},
    1.16 -    @{theory Frontend}, knowledge_parent]) allthys         (*["Isac", ..., "Isac"]*)
    1.17 +    @{theory Frontend}, knowledge_parent]) allthys         (*["Isac_Knowledge", ..., "Isac_Knowledge"]*)
    1.18  
    1.19 -  val isabthys' =                         (*["Complex_Main", "Taylor", .., "Isac"]*)
    1.20 +  val isabthys' =                         (*["Complex_Main", "Taylor", .., "Isac_Knowledge"]*)
    1.21      drop ((find_index (curry Context.eq_thy @{theory Complex_Main}) allthys), allthys);
    1.22 -  val isacthys' =                         (*["Isac", "Inverse_Z_Transform",  .., "KEStore"]*)
    1.23 +  val isacthys' =                         (*["Isac_Knowledge", "Inverse_Z_Transform",  .., "KEStore"]*)
    1.24      take ((find_index (curry Context.eq_thy @{theory Complex_Main}) allthys), allthys);
    1.25  
    1.26 -  val knowthys' =                         (*["Isac", .., "Descript"]*)
    1.27 +  val knowthys' =                         (*["Isac_Knowledge", .., "Descript"]*)
    1.28      take ((find_index (curry Context.eq_thy proglang_parent) isacthys'), isacthys');
    1.29    val progthys' =                         (*["Program", "Tools", "ListC", "KEStore"]*)
    1.30      drop ((find_index (curry Context.eq_thy proglang_parent) isacthys') + 1(*ProgLang*), isacthys');