1.1 --- a/test/Tools/isac/Knowledge/eqsystem-1.sml	Wed Jan 11 11:38:01 2023 +0100
     1.2 +++ b/test/Tools/isac/Knowledge/eqsystem-1.sml	Wed Jan 25 15:52:33 2023 +0100
     1.3 @@ -301,7 +301,7 @@
     1.4       ((Store.Node ("LINEAR", [Problem.from_store ctxt ["LINEAR", "system"]], [])): Problem.T Store.node));
     1.5        val {thy, model, where_, where_rls, ...} = py ;
     1.6  "~~~~~ fun O_Model.init, args:"; val (thy, fmz, pbt) = (thy, fmz, model);
     1.7 -        val ctxt = Proof_Context.init_global thy;
     1.8 +      val (ts, ctxt) = ContextC.build_while_parsing fmz thy;
     1.9  "~~~~~ fun declare_constraints, args:"; val (t, ctxt) = (nth 1 fmz, ctxt);
    1.10        fun get_vars ((v,T)::vs) = (case raw_explode v |> Library.read_int of
    1.11                (_, _::_) => (Free (v,T)::get_vars vs)