1.1 --- a/TODO.md	Tue Aug 10 11:55:24 2021 +0200
     1.2 +++ b/TODO.md	Tue Aug 10 12:56:06 2021 +0200
     1.3 @@ -35,9 +35,6 @@
     1.4  * WN: proper ML antiquotations for "Tactical.Try" etc. --- be careful about unclear situations,
     1.5    e.g. "Tactical.Try" vs. "Lucas_Interpreter.Try";
     1.6  
     1.7 -* WN: check remaining MethodC.prep_input that use a different theory (e.g. "Diff"):
     1.8 -  Is this really required, or can we just use the 'method' command?
     1.9 -
    1.10  * WN: eliminate global flags like "trace_on", replace Unsynchronized.ref by
    1.11      ML \<open>val rewrite_trace = Attrib.setup_config_bool \<^binding>\<open>rewrite_trace\<close> (K false);\<close>
    1.12