1.1 --- a/TODO.md	Wed May 26 16:24:05 2021 +0200
     1.2 +++ b/TODO.md	Tue Jun 01 21:01:32 2021 +0200
     1.3 @@ -37,6 +37,8 @@
     1.4  * WN: remove always empty arguments in MethodC.prep_input and Problem.prep_input
     1.5    (following the "TODO" comment);
     1.6  
     1.7 +* WN: trim-down MethodC.prep_input and Problem.prep_input to what is really needed.
     1.8 +
     1.9  * WN: eliminate ThyC.to_ctxt, use Proof_Context.init_global inline to make more
    1.10    clear where the normal Isabelle context-discipline is bypassed;
    1.11  
    1.12 @@ -59,3 +61,9 @@
    1.13        Left "ASCII art" in case of indicating comments pointing at facts ABOVE.
    1.14  
    1.15  * WN: "fun pr_ord" is not required if used with @{make_string}, @{print}, @{print tracing};
    1.16 +
    1.17 +* WN: eliminate global flags like "trace_on", replace Unsynchronized.ref by
    1.18 +
    1.19 +ML \<open>
    1.20 +  val rewrite_trace = Attrib.setup_config_bool \<^binding>\<open>rewrite_trace\<close> (K false);
    1.21 +\<close>