1.1 --- a/test/Tools/isac/MathEngBasic/mstools.sml	Tue May 12 16:22:00 2020 +0200
     1.2 +++ b/test/Tools/isac/MathEngBasic/mstools.sml	Tue May 12 17:42:29 2020 +0200
     1.3 @@ -60,11 +60,11 @@
     1.4  just_created_ pblobj (*by Subproblem*) andalso origin <> e_origin; (*false=oldNB*)
     1.5  val cpI = if pI = Problem.id_empty then pI' else pI;
     1.6  		val cmI = if mI = e_metID then mI' else mI;
     1.7 -		val {ppc, prls, where_, ...} = get_pbt cpI;
     1.8 +		val {ppc, prls, where_, ...} = Problem.from_store cpI;
     1.9  		val pre = Pre_Conds.check' "thy 100820" prls where_ probl;
    1.10  		val pb = foldl and_ (true, map fst pre);
    1.11  val (_,tac) = nxt_spec p_ pb oris (dI',pI',mI') (probl, meth) 
    1.12 -			    (ppc, (#ppc o get_met) cmI) (dI, pI, mI); (*tac = Add_Given "equality (-1 + x = 0)"*)
    1.13 +			    (ppc, (#ppc o Method.from_store) cmI) (dI, pI, mI); (*tac = Add_Given "equality (-1 + x = 0)"*)
    1.14  "~~~~~ fun Step_Specify.by_tactic_input, args:"; val (Add_Given ct, ptp) = (tac, ptp);
    1.15  "~~~~~ fun nxt_specif_additem, args:"; val (sel, ct, ptp as (pt, (p, Pbl))) = ("#Given", ct, ptp);
    1.16  val (PblObj{meth=met,origin=(oris,(dI',pI',_),_),
    1.17 @@ -72,7 +72,7 @@
    1.18  val thy = if dI = ThyC.id_empty then ThyC.get_theory dI' else ThyC.get_theory dI;
    1.19  val cpI = if pI = Problem.id_empty then pI' else pI;
    1.20  val ctxt = get_ctxt pt (p, Pbl);
    1.21 -"~~~~~ fun add_single, args:"; val (ctxt, sel, oris, ppc, pbt, str) = (ctxt, sel, oris, pbl, ((#ppc o get_pbt) cpI), ct);
    1.22 +"~~~~~ fun add_single, args:"; val (ctxt, sel, oris, ppc, pbt, str) = (ctxt, sel, oris, pbl, ((#ppc o Problem.from_store) cpI), ct);
    1.23  val SOME t = parseNEW ctxt str;
    1.24  is_known ctxt sel oris t;
    1.25  "~~~~~ fun is_known, args:"; val (ctxt, sel, ori, t) = (ctxt, sel, oris, t);
    1.26 @@ -84,7 +84,7 @@
    1.27  (*if Input_Descript.is_a d then () else error "TODO";*)
    1.28  if Input_Descript.is_a d then () else error "TODO";
    1.29  "----- these were the errors (call hierarchy from bottom up)";
    1.30 -I_Model.check_single ctxt sel oris pbl ((#ppc o get_pbt) cpI) ct;(*WAS
    1.31 +I_Model.check_single ctxt sel oris pbl ((#ppc o Problem.from_store) cpI) ct;(*WAS
    1.32  Err "[error] add_single: is_known: identifiers [equality] not in example"*)
    1.33  nxt_specif_additem "#Given" ct ptp;(*WAS
    1.34  Tac "[error] add_single: is_known: identifiers [equality] not in example"*)
    1.35 @@ -248,7 +248,7 @@
    1.36  "----------- fun upds_envv ---------------------------------------------------------------------";
    1.37  (* eval test-maximum.sml until Specify_Method ...
    1.38    val PblObj{probl=(_,pbl),origin=(_,(_,_,mI),_),...} = get_obj I pt [];
    1.39 -  val met = (#ppc o get_met) mI;
    1.40 +  val met = (#ppc o Method.from_store) mI;
    1.41  
    1.42    val envv = [];
    1.43    val eargs = flat eargs;