# HG changeset patch
# User wenzelm
# Date 1622574092 -7200
# Node ID 1c49963adb28170c285d5e375c344552f251fb7d
# Parent  31efa1b39a2004ead7c26988567b0f6669619cdd
more TODO;

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