1.1 --- a/TODO.md	Thu Oct 20 10:47:52 2022 +0200
     1.2 +++ b/TODO.md	Thu Oct 20 12:12:18 2022 +0200
     1.3 @@ -65,6 +65,7 @@
     1.4  * WN: follow up 6: eliminate use of Thy_Info.get_theory
     1.5        follow up 7: ANSWER: represent items, which have not yet been input IN VSCode_Example.thy WITH "__"
     1.6  
     1.7 +* WN: cleanup Problem/MethodC..prep_input
     1.8  * WN: Sub_Problem.tac_from_prog: use ctxt from pt
     1.9  * WN: improve naming in refine.sml, m-match.sml
    1.10  * WN: rename ‹ML_structure KEStore_Elems› to ‹ML_structure Know_Store›

     2.1 --- a/src/Tools/isac/BaseDefinitions/termC.sml	Thu Oct 20 10:47:52 2022 +0200
     2.2 +++ b/src/Tools/isac/BaseDefinitions/termC.sml	Thu Oct 20 12:12:18 2022 +0200
     2.3 @@ -75,8 +75,7 @@
     2.4    val parseNEW: Proof.context -> string -> term option(*old version to be eliminated*)
     2.5    val parseNEW': Proof.context -> string -> term      (*old version to be eliminated*)
     2.6    val parseNEW'': theory -> string -> term            (*old version to be eliminated*)
     2.7 -  val parse_strict: theory -> string -> term          (*to be replaced by parse, typ_a2real for CAS_Cmd*)
     2.8 -  val parse_strict_PIDE: theory -> string -> term     (*to be 1.replaced by parse_patt*)
     2.9 +  val parse_strict: theory -> string -> term     (*to be 1.replaced by parse_patt*)
    2.10  (*goal*)val parse: Proof.context -> string -> term
    2.11    val parse_patt_PIDE: theory -> string -> term       (*rename to parse_patt*)
    2.12  (*goal*)val parse_patt: theory -> string -> term      (*with typ_a2real still for tests *)
    2.13 @@ -562,10 +561,8 @@
    2.14    | NONE => raise TERM ("NO parseNEW'' for " ^ str, [])
    2.15  (*\----- old versions to be eliminated -------------------------------------------------------/*)
    2.16  
    2.17 -(* to be replaced by parse-test..*)
    2.18 -fun parse_strict thy str = typ_a2real (Syntax.read_term_global thy str); (*still for CAS_Cmd*)
    2.19  (* to be replaced by parse..*)
    2.20 -fun parse_strict_PIDE thy str = (*typ_a2real*) (Syntax.read_term_global thy str);
    2.21 +fun parse_strict thy str = (*typ_a2real*) (Syntax.read_term_global thy str);
    2.22  fun parse ctxt str = Syntax.read_term_global (Proof_Context.theory_of ctxt) str;
    2.23  (* parse term patterns; Var ("v",_), i.e. "?v", are required for instantiation *)
    2.24  (*rename to parse_patt..*)

     3.1 --- a/src/Tools/isac/Build_Isac.thy	Thu Oct 20 10:47:52 2022 +0200
     3.2 +++ b/src/Tools/isac/Build_Isac.thy	Thu Oct 20 12:12:18 2022 +0200
     3.3 @@ -165,19 +165,6 @@
     3.4  ML \<open>
     3.5  \<close> ML \<open>
     3.6  \<close> ML \<open>
     3.7 -\<close> ML \<open> (*\<longrightarrow> ThyC*)
     3.8 -fun get_theory_PIDE ctxt thy_id =
     3.9 -  let
    3.10 -    val known_thys = Theory.nodes_of (Proof_Context.theory_of ctxt)
    3.11 -  in 
    3.12 -    (find_first (fn thy => Context.theory_name thy = thy_id) known_thys
    3.13 -      |> the)
    3.14 -    handle Option.Option => raise ERROR ("get_theory fails with " ^ quote thy_id)
    3.15 -  end
    3.16 -\<close> ML \<open>
    3.17 -get_theory_PIDE: Proof.context -> ThyC.id -> theory
    3.18 -\<close> ML \<open>
    3.19 -the
    3.20  \<close> ML \<open>
    3.21  \<close> ML \<open>
    3.22  \<close>