1.1 --- a/src/Tools/isac/MathEngine/mathengine-stateless.sml	Fri Oct 07 20:46:48 2022 +0200
     1.2 +++ b/src/Tools/isac/MathEngine/mathengine-stateless.sml	Sat Oct 08 11:40:48 2022 +0200
     1.3 @@ -140,7 +140,7 @@
     1.4    	  if pI' = Problem.id_empty 
     1.5    		then (* TODO.WN051125 (#init o get_pbt) pI *) takelast (2, pI)
     1.6    		else pI'
     1.7 -  	val {ppc, where_, prls, ...} = Problem.from_store_PIDE ctxt pblID
     1.8 +  	val {ppc, where_, prls, ...} = Problem.from_store ctxt pblID
     1.9    	val (model_ok, (pbl, pre)) = M_Match.match_itms_oris (ThyC.get_theory "Isac_Knowledge") probl (ppc, where_, prls) os
    1.10    in
    1.11      (model_ok, pblID, hdl, pbl, pre)
    1.12 @@ -156,7 +156,7 @@
    1.13    	val metID = if mI' = MethodC.id_empty 
    1.14    		    then (*TODO.WN051125 (#init o get_pbt) pI *) takelast (2, mI)
    1.15    		    else mI'
    1.16 -  	val {ppc, pre, prls, scr, ...} = MethodC.from_store_PIDE ctxt metID
    1.17 +  	val {ppc, pre, prls, scr, ...} = MethodC.from_store ctxt metID
    1.18    	val (model_ok, (pbl, pre)) = M_Match.match_itms_oris (ThyC.get_theory "Isac_Knowledge") meth (ppc,pre,prls) os
    1.19    in
    1.20      (model_ok, metID, scr, pbl, pre)
    1.21 @@ -170,7 +170,7 @@
    1.22          Ctree.PblObj {probl, origin = (os, ospec, hdl), spec, ...} => (probl, os, ospec, hdl, spec)
    1.23        | Ctree.PrfObj _ => raise ERROR "context_pbl: uncovered case"
    1.24      val ctxt = spec |> References.select_input ospec |> #1 |> ThyC.get_theory |> Proof_Context.init_global
    1.25 -  	val {ppc, where_, prls, ...} = Problem.from_store_PIDE ctxt pI
    1.26 +  	val {ppc, where_, prls, ...} = Problem.from_store ctxt pI
    1.27    	val (model_ok, (pbl, pre)) = M_Match.match_itms_oris (ThyC.get_theory "Isac_Knowledge") probl (ppc,where_,prls) os
    1.28    in
    1.29      (model_ok, pI, hdl, pbl, pre)
    1.30 @@ -182,7 +182,7 @@
    1.31        case Ctree.get_obj I pt p of
    1.32          Ctree.PblObj {meth, origin = (os, _, _), ctxt, ...} => (meth, os, ctxt)
    1.33        | Ctree.PrfObj _ => raise ERROR "context_met: uncovered case"
    1.34 -  	val {ppc,pre,prls,scr,...} = MethodC.from_store_PIDE ctxt mI
    1.35 +  	val {ppc,pre,prls,scr,...} = MethodC.from_store ctxt mI
    1.36    	val (model_ok, (pbl, pre)) = M_Match.match_itms_oris (ThyC.get_theory "Isac_Knowledge") meth (ppc,pre,prls) os
    1.37    in
    1.38      (model_ok, mI, scr, pbl, pre)
    1.39 @@ -199,7 +199,7 @@
    1.40      case Refine.problem (ThyC.get_theory "Isac_Knowledge") pI probl of
    1.41    	  NONE => (*copy from context_pbl*)
    1.42    	    let
    1.43 -  	      val {ppc, where_, prls, ...} = Problem.from_store_PIDE ctxt pI
    1.44 +  	      val {ppc, where_, prls, ...} = Problem.from_store ctxt pI
    1.45    	      val (_, (pbl, pre)) = M_Match.match_itms_oris (ThyC.get_theory "Isac_Knowledge") probl (ppc,where_,prls) os
    1.46          in
    1.47            (false, pI, hdl, pbl, pre)