1.1 --- a/TODO.md	Sat Jun 12 18:30:31 2021 +0200
     1.2 +++ b/TODO.md	Sat Jun 12 18:33:15 2021 +0200
     1.3 @@ -2,13 +2,8 @@
     1.4    + consider in Build_Thydata:  Thy_Hierarchy.insert_errpatIDs
     1.5    + consider in Biegelinie.thy: KEStore_Elems.add_thes, 
     1.6  
     1.7 -* MW: ML antiqutation @{rule_thm NAME} to produce (Rule.Thm ("NAME", ThmC.numerals_to_Free "NAME"));
     1.8 -
     1.9  * MW: check uses of Unsynchronized.ref vs. Synchronized.var;
    1.10  
    1.11 -* MW: proper formal name space for rule set, model patterns, methods;
    1.12 -  proper setup command;
    1.13 -
    1.14  * MW: clarify/eliminate Isabelle/Scala add-ons (presently unused)
    1.15  
    1.16      diff -r /home/makarius/isabelle/repos-Isabelle2021/src/Pure/build-jars ./src/Pure/build-jars
    1.17 @@ -19,19 +14,9 @@
    1.18      76a77
    1.19      >       "src/Tools/isac/etc" -> Path.explode("isabelle.isac"),
    1.20  
    1.21 -* MW: when Isabelle inner syntax is processed literally in Isabelle/ML, prefer formal Input.source
    1.22 -with literal \<open>...\<close> instead of old-fashioned "..."; this will eventually allow automated update of
    1.23 -old ASCII notation (e.g. "EX" vs. "\<exists>"), with the help of PIDE markup;
    1.24 -
    1.25  
    1.26  * Clarify symmetric rule: Thm.apply_attribute Calculation.symmetric thm context (!?);
    1.27  
    1.28 -* Clarify rule_set "prog_expr": avoid rebinding!?
    1.29 -
    1.30 -* rule_set: proper name space and declaration order (!?);
    1.31 -
    1.32 -* Avoid Thm.get_name_hint --- somewhat fragile.
    1.33 -
    1.34  * Is it possible to eliminate union_overwrite, in favour of more standard data
    1.35    add/merge discipline?
    1.36  
    1.37 @@ -42,6 +27,8 @@
    1.38  * Eliminate mutable Rewrite_Ord.rew_ord' (!?);
    1.39  
    1.40  
    1.41 +* WN: Avoid Thm.get_name_hint --- somewhat fragile.
    1.42 +
    1.43  * WN: clarify Rule.Thm ("minus_divide_left", ...): Should this be @{rule_thm_sym} antiquotation?
    1.44  
    1.45  * WN: remove always empty arguments in MethodC.prep_input and Problem.prep_input