1.1 --- a/TODO.md	Wed May 26 13:42:53 2021 +0200
     1.2 +++ b/TODO.md	Wed May 26 14:10:17 2021 +0200
     1.3 @@ -31,6 +31,16 @@
     1.4  * Check/clarify Context.theory_name vs. Context.theory_long_name.
     1.5  
     1.6  
     1.7 +* WN: remove always empty arguments in MethodC.prep_input and Problem.prep_input
     1.8 +  (following the "TODO" comment);
     1.9 +
    1.10 +* WN: eliminate ThyC.to_ctxt, use Proof_Context.init_global inline to make more
    1.11 +  clear where the normal Isabelle context-discipline is bypassed;
    1.12 +
    1.13 +* WN: standardize theory for KEStore_Elems.add_rlss, KEStore_Elems.add_mets, KEStore_Elems.add_pbts
    1.14 +    - should be always the current @{theory} of the enclosing "setup" command;
    1.15 +    - avoid old-style "val thy = @{theory}" somewhere in a theory file;
    1.16 +
    1.17  * WN: more direct logical foundations wrt. Isabelle/HOL, eliminate many axiomatizations
    1.18      - quite often "axiomatization ..." can be turned into "lemma ... by auto"
    1.19        without further ado;