1.1 --- a/test/Tools/isac/Minisubpbl/150a-add-given-Maximum.sml	Sat Feb 04 17:00:25 2023 +0100
     1.2 +++ b/test/Tools/isac/Minisubpbl/150a-add-given-Maximum.sml	Tue Feb 07 17:25:09 2023 +0100
     1.3 @@ -93,10 +93,10 @@
     1.4        (*case*) find_first (I_Model.is_error o #5) pbl (*of*);
     1.5  
     1.6          (*case*)
     1.7 -   Specify.item_to_add (ThyC.get_theory_PIDE ctxt
     1.8 +   Specify.item_to_add (ThyC.get_theory ctxt
     1.9              (if dI = ThyC.id_empty then dI' else dI)) oris pbt pbl (*of*);
    1.10  "~~~~~ fun item_to_add , args:"; val (thy, oris, _, itms)
    1.11 -  = ((ThyC.get_theory_PIDE ctxt (if dI = ThyC.id_empty then dI' else dI)), oris, pbt, pbl);
    1.12 +  = ((ThyC.get_theory ctxt (if dI = ThyC.id_empty then dI' else dI)), oris, pbt, pbl);
    1.13        fun testr_vt v ori = member op= (#2 (ori : O_Model.single)) v andalso (#3 ori) <> "#undef"
    1.14        fun testi_vt v itm = member op= (#2 (itm : I_Model.single)) v
    1.15        fun test_id ids r = member op= ids (#1 (r : O_Model.single))
    1.16 @@ -262,7 +262,7 @@
    1.17        val (oris, dI, dI', pI', probl, ctxt) = case get_obj I pt p of
    1.18          PblObj {origin = (oris, (dI,_,_),_), spec = (dI',pI',_), probl, ctxt, ...} =>
    1.19            (oris, dI, dI', pI', probl, ctxt)
    1.20 -	    val thy = ThyC.get_theory_PIDE ctxt (if dI' = ThyC.id_empty then dI else dI');
    1.21 +	    val thy = ThyC.get_theory ctxt (if dI' = ThyC.id_empty then dI else dI');
    1.22        val {model, where_, where_rls,...} = Problem.from_store (Ctree.get_ctxt pt pos) pI
    1.23  (*\\------------------ step into do_next ---------------------------------------------------//*)
    1.24  (*\------------------- step into me Specify_Theory -----------------------------------------//*)
    1.25 @@ -291,7 +291,7 @@
    1.26  		    val (oris, dI, pI, dI', pI', itms) = case Ctree.get_obj I pt p of
    1.27  		      Ctree.PblObj {origin = (oris, (dI, pI, _), _), spec = (dI', pI', _), probl = itms, ...}
    1.28  		        => (oris, dI, pI, dI', pI', itms)
    1.29 -	      val thy = ThyC.get_theory_PIDE ctxt (if dI' = ThyC.id_empty then dI else dI');
    1.30 +	      val thy = ThyC.get_theory ctxt (if dI' = ThyC.id_empty then dI else dI');
    1.31  (*\\------------------ step into by_tactic -------------------------------------------------//*)
    1.32  val ("ok", (_, _, ptp as (pt, p))) = return_by_tactic (* kept for continuing me *);
    1.33  
    1.34 @@ -329,7 +329,7 @@
    1.35      val {model = m_patt, where_, where_rls, ...} = MethodC.from_store ctxt mID
    1.36      val {origin = (root_model, _, _), ...} = Calc.specify_data (ctree, ([], Pos.Und))
    1.37      val (o_model', ctxt') = O_Model.complete_for m_patt root_model (o_model, ctxt)
    1.38 -    val thy = ThyC.get_theory_PIDE ctxt dI
    1.39 +    val thy = ThyC.get_theory ctxt dI
    1.40      val (_, (i_model, _)) = M_Match.match_itms_oris ctxt i_prob (m_patt, where_, where_rls) o_model';
    1.41  (*\------------------- step into me Specify_Problem ----------------------------------------//*)
    1.42  val (p,_,f,nxt,_,pt) = return_me_Specify_Problem
    1.43 @@ -379,10 +379,10 @@
    1.44      (*case*) find_first (I_Model.is_error o #5) met (*of*);
    1.45  
    1.46        (*case*)
    1.47 -   Specify.item_to_add (ThyC.get_theory_PIDE ctxt 
    1.48 +   Specify.item_to_add (ThyC.get_theory ctxt 
    1.49       (if dI = ThyC.id_empty then dI' else dI)) oris mpc met (*of*);
    1.50  "~~~~~ fun item_to_add , args:"; val (thy, oris, _, itms)
    1.51 -  = ((ThyC.get_theory_PIDE ctxt (if dI = ThyC.id_empty then dI' else dI)), oris, mpc, met);
    1.52 +  = ((ThyC.get_theory ctxt (if dI = ThyC.id_empty then dI' else dI)), oris, mpc, met);
    1.53  (*\------------------- step into me Specify_Method -----------------------------------------//*)
    1.54  val (p,_,f,nxt,_,pt) = return_me_Add_Given_FunctionVariable
    1.55