1.1 --- a/src/Tools/isac/TODO.thy	Wed Mar 11 15:25:52 2020 +0100
     1.2 +++ b/src/Tools/isac/TODO.thy	Tue Mar 17 14:50:19 2020 +0100
     1.3 @@ -143,6 +143,7 @@
     1.4    \item xxx
     1.5    \item generate, generate1: NO thy as arg.
     1.6          Generate.generate1 thy is redundant: is the same during pbl, thus lookup spec
     1.7 +        redesign return value (originally for output by fun me?)
     1.8    \item xxx
     1.9    \item shift tests into NEW model.sml (upd, upds_envv, ..)
    1.10    \item xxx
    1.11 @@ -157,7 +158,7 @@
    1.12        rm Assumptions  :: bool  (* TODO: remove with making ^^^ idle *)
    1.13      \item xxx
    1.14      \item xxx
    1.15 -    \item remove ctxt from Tactic.T; this makes use of ctxt more explicit (e.g. in LI)
    1.16 +    \item remove ctxt from Tactic.Subproblem'; this makes use of ctxt more explicit (e.g. in LI)
    1.17        \begin{itemize}
    1.18        \item Tactic.Apply_Method' (mI, _, _, _(*ctxt ?!?*))) .. remove ctxt
    1.19        \item rm ctxt from Subproblem' (is separated in associate!))