test/Tools/isac/MathEngine/mathengine-stateless.sml
changeset 60651 b7a2ad3b3d45
parent 60618 46f1c75d4f75
child 60652 75003e8f96ab
     1.1 --- a/test/Tools/isac/MathEngine/mathengine-stateless.sml	Wed Jan 11 11:38:01 2023 +0100
     1.2 +++ b/test/Tools/isac/MathEngine/mathengine-stateless.sml	Wed Jan 25 15:52:33 2023 +0100
     1.3 @@ -122,8 +122,7 @@
     1.4  	    val thy = ThyC.get_theory dI
     1.5  	    val ctxt = Proof_Context.init_global thy;
     1.6          (*if*) mI = ["no_met"](*else*);
     1.7 -	          val pors = Problem.from_store ctxt pI |> #model |> O_Model.init thy fmz;
     1.8 -            val pctxt = ContextC.initialise' thy fmz;
     1.9 +	         val (pors, pctxt) = Problem.from_store ctxt pI |> #model |> O_Model.init_PIDE thy fmz;
    1.10  	      val {cas, model, thy=thy',...} = Problem.from_store ctxt pI; (*take dI from _refined_ pbl*)
    1.11  	"tracing bottom up"; Context.theory_name thy' = "Build_Inverse_Z_Transform"; (*WAS true*)
    1.12        val dI = Context.theory_name (ThyC.parent_of thy thy');