1.1 --- a/TODO.md	Thu May 26 12:53:13 2022 +0200
     1.2 +++ b/TODO.md	Fri May 27 12:07:55 2022 +0200
     1.3 @@ -59,8 +59,6 @@
     1.4      (*1*)val _ = tracing ("hd_ord (f, g)      = " ^ ((pr_ord o hd_ord) (f, g)) );
     1.5      (*2*)val _ = @{print tracing}{a = "hd_ord (f, g)      = ", z = hd_ord (f, g)}(**)
     1.6  
     1.7 -* WN: first parse with ctxt in Specify (O_Model.init shall return a context,..) etc
     1.8 -
     1.9  
    1.10  * WN: eliminate global flags like "trace_on", replace Unsynchronized.ref by
    1.11  

     2.1 --- a/src/Tools/isac/MathEngBasic/ctree-basic.sml	Thu May 26 12:53:13 2022 +0200
     2.2 +++ b/src/Tools/isac/MathEngBasic/ctree-basic.sml	Fri May 27 12:07:55 2022 +0200
     2.3 @@ -188,8 +188,8 @@
     2.4  	           term,            (* headline of calc-head, as calculated initially(!)             *)
     2.5      spec  : References_Def.T, (* explicitly input                                              *)
     2.6      probl : Model_Def.i_model,(* = I_Model.T for interactive input to a Problem                *)
     2.7 -    meth  : Model_Def.i_model,(* = I_Model.T for interactive input to a MethodC                 *)
     2.8 -    ctxt  : Proof.context,    (* used while specifying this (Sub-)Problem and MethodC           *)
     2.9 +    meth  : Model_Def.i_model,(* = I_Model.T for interactive input to a MethodC                *)
    2.10 +    ctxt  : Proof.context,    (* used while specifying this (Sub-)Problem and MethodC          *)
    2.11      loc   : (Istate_Def.T * Proof.context) option  (* like in PrfObj, calling this SubProblem  *)
    2.12            * (Istate_Def.T * Proof.context) option, (* like in PrfObj, finishing the SubProblem *)
    2.13      branch: branch,           (* like PrfObj                                                   *)
    2.14 @@ -470,9 +470,9 @@
    2.15  fun get_ctxt pt (pos as (p, p_)) =
    2.16    if member op = [Frm, Res] p_
    2.17    then get_loc pt pos |> #2 (*for program interpretation rely on fun get_loc*)
    2.18 -  else                      (*for specify phase take ctx from PblObj        *)
    2.19 +  else             (*p = Pbl: for specify phase take ctx from PblObj        *)
    2.20      if (p |> get_obj g_origin pt |> LibraryC.fst3) = [] (*CAS-command ?     *)
    2.21 -    then (ThyC.get_theory "Isac_Knowledge") |> Defs.global_context |> fst
    2.22 +    then (ThyC.get_theory "Isac_Knowledge"(*CAS-command unknown*)) |> Defs.global_context |> fst
    2.23      else get_obj g_ctxt pt p
    2.24  
    2.25  fun get_assumptions pt p = get_ctxt pt p |> ContextC.get_assumptions;

     3.1 --- a/test/Tools/isac/Specify/o-model.sml	Thu May 26 12:53:13 2022 +0200
     3.2 +++ b/test/Tools/isac/Specify/o-model.sml	Fri May 27 12:07:55 2022 +0200
     3.3 @@ -17,10 +17,10 @@
     3.4  "-----------------------------------------------------------------------------------------------";
     3.5  "-----------------------------------------------------------------------------------------------";
     3.6  
     3.7 +"----------- fun init for O_Model.T ------------------------------------------------------------";
     3.8 +"----------- fun init for O_Model.T ------------------------------------------------------------";
     3.9 +"----------- fun init for O_Model.T ------------------------------------------------------------";
    3.10  open O_Model;
    3.11 -"----------- fun init for O_Model.T ------------------------------------------------------------";
    3.12 -"----------- fun init for O_Model.T ------------------------------------------------------------";
    3.13 -"----------- fun init for O_Model.T ------------------------------------------------------------";
    3.14  val f_model = ["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",
    3.15  	"Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]",
    3.16  	"FunktionsVariable x", "GleichungsVariablen [c, c_2, c_3, c_4]",