1.1 --- a/test/Tools/isac/Minisubpbl/150-add-given.sml	Tue May 12 16:22:00 2020 +0200
     1.2 +++ b/test/Tools/isac/Minisubpbl/150-add-given.sml	Tue May 12 17:42:29 2020 +0200
     1.3 @@ -34,17 +34,17 @@
     1.4  just_created_ pblobj (*by Subproblem*) andalso origin <> e_origin; (* = false*)
     1.5          val cpI = if pI = Problem.id_empty then pI' else pI;
     1.6  		    val cmI = if mI = Method.id_empty 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  
    1.12  (*    val (_,tac) = nxt_spec p_ pb oris (dI',pI',mI') (probl, meth) 
    1.13 -			    (ppc, (#ppc o get_met) cmI) (dI, pI, mI);
    1.14 +			    (ppc, (#ppc o Method.from_store) cmI) (dI, pI, mI);
    1.15  ERROR: val tac = Add_Given "equality (<markup> + <markup> = <markup>)"*)
    1.16  "~~~~~ fun nxt_spec, args:"; val (Pbl, preok, (oris : O_Model.T), ((dI', pI', mI') : Spec.T),
    1.17    ((pbl : I_Model.T), (met : I_Model.T)), (pbt, mpc), ((dI, pI, mI) : Spec.T)) = 
    1.18    (p_, pb, oris, (dI',pI',mI'), (probl, meth), 
    1.19 -			    (ppc, (#ppc o get_met) cmI), (dI, pI, mI));
    1.20 +			    (ppc, (#ppc o Method.from_store) cmI), (dI, pI, mI));
    1.21  
    1.22  dI' = ThyC.id_empty andalso dI = ThyC.id_empty; (* = false*)
    1.23  pI' = Problem.id_empty andalso pI = Problem.id_empty; (* = false*)