1.1 --- a/src/Tools/isac/TODO.thy	Wed Apr 15 16:46:41 2020 +0200
     1.2 +++ b/src/Tools/isac/TODO.thy	Wed Apr 15 18:00:58 2020 +0200
     1.3 @@ -152,7 +152,7 @@
     1.4    \item ? what is the difference headline <--> cascmd in
     1.5      Subproblem' (spec, oris, headline, fmz_, context, cascmd)
     1.6    \item xxx
     1.7 -  \item inform: TermC.parse (Celem.assoc_thy "Isac_Knowledge") istr --> parseNEW context istr
     1.8 +  \item inform: TermC.parse (ThyC.get_theory "Isac_Knowledge") istr --> parseNEW context istr
     1.9    \item xxx
    1.10    \item unify/clarify stac2tac_ | 
    1.11      \begin{itemize}
    1.12 @@ -406,7 +406,7 @@
    1.13    \item 1. Rewrite.eval_true_, then
    1.14      LItool.check_leaf, Rewrite.eval_prog_expr, Generate.generate1, LItool.tac_from_prog.
    1.15    \item fun associate
    1.16 -    let val thy = Celem.assoc_thy "Isac_Knowledge";(*TODO*)
    1.17 +    let val thy = ThyC.get_theory "Isac_Knowledge";(*TODO*)
    1.18    \item xxx
    1.19    \item xxx
    1.20    \item in locate_input_tactic .. ?scan_dn1?; Program.is_eval_expr   .use  Term.exists_Const