test/Tools/isac/Knowledge/eqsystem-1.sml
changeset 60469 89e1d8a633bb
parent 60424 c3acf9c442ac
child 60500 59a3af532717
     1.1 --- a/test/Tools/isac/Knowledge/eqsystem-1.sml	Mon Jun 20 11:55:55 2022 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/eqsystem-1.sml	Mon Jun 20 18:37:54 2022 +0200
     1.3 @@ -298,7 +298,7 @@
     1.4     ((rev o tl) pblID, fmz, [(*match list*)],
     1.5       ((Store.Node ("LINEAR", [Problem.from_store ["LINEAR", "system"]], [])): Problem.T Store.node));
     1.6        val {thy, ppc, where_, prls, ...} = py ;
     1.7 -"~~~~~ fun O_Model.init, args:"; val (fmz, thy, pbt) = (fmz, thy, ppc);
     1.8 +"~~~~~ fun O_Model.init, args:"; val (thy, fmz, pbt) = (thy, fmz, ppc);
     1.9          val ctxt = Proof_Context.init_global thy;
    1.10  "~~~~~ fun declare_constraints, args:"; val (t, ctxt) = (nth 1 fmz, ctxt);
    1.11        fun get_vars ((v,T)::vs) = (case raw_explode v |> Library.read_int of