1.1 --- a/test/Tools/isac/Knowledge/eqsystem-1.sml	Mon Oct 31 18:28:36 2022 +0100
     1.2 +++ b/test/Tools/isac/Knowledge/eqsystem-1.sml	Mon Nov 07 17:37:20 2022 +0100
     1.3 @@ -299,8 +299,8 @@
     1.4  "~~~~~ fun refin' , args:"; val ((pblRD: Problem.id_reverse), fmz, pbls, ((Store.Node (pI, [py], [])): Problem.T Store.node)) =
     1.5     ((rev o tl) pblID, fmz, [(*match list*)],
     1.6       ((Store.Node ("LINEAR", [Problem.from_store ctxt ["LINEAR", "system"]], [])): Problem.T Store.node));
     1.7 -      val {thy, ppc, where_, prls, ...} = py ;
     1.8 -"~~~~~ fun O_Model.init, args:"; val (thy, fmz, pbt) = (thy, fmz, ppc);
     1.9 +      val {thy, model, where_, where_rls, ...} = py ;
    1.10 +"~~~~~ fun O_Model.init, args:"; val (thy, fmz, pbt) = (thy, fmz, model);
    1.11          val ctxt = Proof_Context.init_global thy;
    1.12  "~~~~~ fun declare_constraints, args:"; val (t, ctxt) = (nth 1 fmz, ctxt);
    1.13        fun get_vars ((v,T)::vs) = (case raw_explode v |> Library.read_int of