1.1 --- a/test/Tools/isac/Specify/o-model.sml	Fri Sep 16 12:13:23 2022 +0200
     1.2 +++ b/test/Tools/isac/Specify/o-model.sml	Mon Sep 26 10:57:53 2022 +0200
     1.3 @@ -34,16 +34,19 @@
     1.4  (*  val ((pt, p), tacis) =*)
     1.5  Step_Specify.nxt_specify_init_calc (fmz, sp);
     1.6  "~~~~~ fun nxt_specify_init_calc , args:"; val (fmz, (dI, pI, mI)) = (fmz, sp);
     1.7 -	    val thy = ThyC.get_theory dI;
     1.8 +	    (*val (_, hdl, (dI, pI, mI), pors, pctxt) = *)
     1.9 +           initialise_PIDE (fmz, (dI, pI, mI));
    1.10 +"~~~~~ fun initialise_PIDE , args:"; val (fmz, (dI, pI, mI)) = (fmz, sp);
    1.11 +	    val thy = ThyC.get_theory dI
    1.12 +	    val ctxt = Proof_Context.init_global thy;
    1.13  	      (*if*) mI = ["no_met"] (*else*);
    1.14 -      val (pI, pors, mI) = (pI, Problem.from_store pI |> #ppc |> init thy fmz, mI);
    1.15 +	          val pors = Problem.from_store_PIDE ctxt pI |> #ppc |> O_Model.init thy fmz; (*..TermC.parseNEW'*)
    1.16 +(*+*)Problem.from_store_PIDE ctxt pI: Problem.T;
    1.17 +(*+*)(Problem.from_store_PIDE ctxt pI |> #ppc): Model_Pattern.T;
    1.18  
    1.19 -(*+*)Problem.from_store pI: Problem.T;
    1.20 -(*+*)(Problem.from_store pI |> #ppc): Model_Pattern.T;
    1.21 -
    1.22 -(*+*)val o_model = (Problem.from_store pI |> #ppc |>
    1.23 +(*+*)val o_model = (Problem.from_store_PIDE ctxt pI |> #ppc |>
    1.24     O_Model.init thy fmz);
    1.25 -"~~~~~ fun init , args:"; val (fmz, thy, pbt) = (fmz, thy, Problem.from_store pI |> #ppc);
    1.26 +"~~~~~ fun init , args:"; val (fmz, thy, pbt) = (fmz, thy, Problem.from_store_PIDE ctxt pI |> #ppc);
    1.27        val ori = (map (fn str => str
    1.28                       |> TermC.parseNEW'' thy
    1.29                       |> Input_Descript.split
    1.30 @@ -173,7 +176,7 @@
    1.31  	"interval {x::real. 0 <= x & x <= pi}",
    1.32  	"errorBound (eps=(0::real))"]
    1.33  val pbt as {ppc = ppc,...} =
    1.34 -    Problem.from_store ["maximum_of", "function"];
    1.35 +    Problem.from_store_PIDE @{context} ["maximum_of", "function"];
    1.36  val o_model = O_Model.init @{theory} formalise ppc;
    1.37  
    1.38  case o_model of
    1.39 @@ -279,4 +282,3 @@
    1.40  case O_Model.copy_name pbt oris (hd cy) of
    1.41      ([1], "#Find", Const (\<^const_name>\<open>EqSystem.solution\<close>, _), [Free ("ss'''", _)]) => ()
    1.42    | _ => error "calchead.sml regr.test O_Model.copy_name-2-";
    1.43 -