1.1 --- a/TODO.md	Tue Aug 10 19:05:59 2021 +0200
     1.2 +++ b/TODO.md	Wed Aug 11 11:54:07 2021 +0200
     1.3 @@ -16,6 +16,7 @@
     1.4      cf. e587c45cae0f note in Build_Thydata.thy
     1.5  
     1.6  * Clarify symmetric rule: Thm.apply_attribute Calculation.symmetric thm context (!?);
     1.7 +    ??
     1.8  
     1.9  * KEStore_Elems: Should we eliminate union_overwrite and use standard namespace merge?
    1.10    (Exception: rlss with its special cross-theory merge.)
    1.11 @@ -24,6 +25,9 @@
    1.12      ??
    1.13  
    1.14  * Check/clarify Context.theory_name vs. Context.theory_long_name.
    1.15 +    present ISAC assumes 2 sessions in the MathEngine, Specify and Interpret, 
    1.16 +    and all Isac_Knowledge is in session Isac.
    1.17 +    So Context.theory_name suffices
    1.18  
    1.19  * Eliminate mutable Rewrite_Ord.rew_ord' (!?);
    1.20      shall be done in connection with cf. e587c45cae0f note in Build_Thydata.thy

     2.1 --- a/src/Tools/isac/Knowledge/Build_Thydata.thy	Tue Aug 10 19:05:59 2021 +0200
     2.2 +++ b/src/Tools/isac/Knowledge/Build_Thydata.thy	Wed Aug 11 11:54:07 2021 +0200
     2.3 @@ -69,9 +69,7 @@
     2.4  \<close> 
     2.5  declare[[ML_print_depth = 999]]
     2.6  ML \<open>
     2.7 -map Context.theory_name progthys'
     2.8  \<close> ML \<open>
     2.9 -[] : MethodC.T list
    2.10  \<close> ML \<open>
    2.11  \<close>
    2.12