1.1 --- a/test/Tools/isac/Knowledge/eqsystem.sml	Tue May 12 16:22:00 2020 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/eqsystem.sml	Tue May 12 17:42:29 2020 +0200
     1.3 @@ -285,7 +285,7 @@
     1.4  "~~~~~ fun Refine.refine, args:"; val ((fmz: Formalise.model), (pblID:Problem.id)) = (fmz, ["LINEAR","system"]);
     1.5  "~~~~~ fun refin', args:"; val ((pblRD: pblRD), fmz, pbls, ((Store.Node (pI, [py], [])): Problem.T Store.node)) =
     1.6     ((rev o tl) pblID, fmz, [(*match list*)],
     1.7 -     ((Store.Node ("LINEAR", [get_pbt ["LINEAR","system"]], [])): Problem.T Store.node));
     1.8 +     ((Store.Node ("LINEAR", [Problem.from_store ["LINEAR","system"]], [])): Problem.T Store.node));
     1.9        val {thy, ppc, where_, prls, ...} = py ;
    1.10  "~~~~~ fun O_Model.init, args:"; val (fmz, thy, pbt) = (fmz, thy, ppc);
    1.11          val ctxt = Proof_Context.init_global thy;
    1.12 @@ -430,7 +430,7 @@
    1.13  (*-----fun refin' (pblRD:pblRD) fmz pbls ((Store.Node (pI,[py],[])):pbt Store.store) =
    1.14  (* val ((pblRD:pblRD), fmz, pbls, ((Store.Node (pI,[py],[])):pbt Store.store)) =
    1.15         (rev ["LINEAR","system"], fmz, [(*match list*)],
    1.16 -	((Store.Node ("2x2",[get_pbt ["2x2","LINEAR","system"]],[])):pbt Store.store));
    1.17 +	((Store.Node ("2x2",[Problem.from_store ["2x2","LINEAR","system"]],[])):pbt Store.store));
    1.18     *)
    1.19  > show_types:=true; UnparseC.term (hd where_); show_types:=false;
    1.20  val it = "length_ (es_::real list) = (2::real)" : string
    1.21 @@ -454,7 +454,7 @@
    1.22  val it = "es_::bool list" : string
    1.23  ~~~~~~~~~~~~~~~^^^^^^^^^ OK~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    1.24  
    1.25 -> val {where_,...} = get_pbt ["2x2", "LINEAR","system"];
    1.26 +> val {where_,...} = Problem.from_store ["2x2", "LINEAR","system"];
    1.27  > show_types:=true; UnparseC.term (hd where_); show_types:=false;
    1.28  
    1.29  =========================================================================/