1.1 --- a/test/Tools/isac/Knowledge/eqsystem-1.sml	Fri Oct 07 20:46:48 2022 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/eqsystem-1.sml	Sat Oct 08 11:40:48 2022 +0200
     1.3 @@ -297,7 +297,7 @@
     1.4  "~~~~~ fun Refine.refine , args:"; val ((fmz: Formalise.model), (pblID:Problem.id)) = (fmz, ["LINEAR", "system"]);
     1.5  "~~~~~ fun refin' , args:"; val ((pblRD: Problem.id_reverse), fmz, pbls, ((Store.Node (pI, [py], [])): Problem.T Store.node)) =
     1.6     ((rev o tl) pblID, fmz, [(*match list*)],
     1.7 -     ((Store.Node ("LINEAR", [Problem.from_store_PIDE ctxt ["LINEAR", "system"]], [])): Problem.T Store.node));
     1.8 +     ((Store.Node ("LINEAR", [Problem.from_store ctxt ["LINEAR", "system"]], [])): Problem.T Store.node));
     1.9        val {thy, ppc, where_, prls, ...} = py ;
    1.10  "~~~~~ fun O_Model.init, args:"; val (thy, fmz, pbt) = (thy, fmz, ppc);
    1.11          val ctxt = Proof_Context.init_global thy;