120 Step_Specify.initialise ctxt (fmz, (dI, pI, mI)); |
120 Step_Specify.initialise ctxt (fmz, (dI, pI, mI)); |
121 "~~~~~ fun initialise , args:"; val (fmz, (dI, pI, mI)) = (fmz, (dI, pI, mI)); |
121 "~~~~~ fun initialise , args:"; val (fmz, (dI, pI, mI)) = (fmz, (dI, pI, mI)); |
122 val thy = ThyC.get_theory dI |
122 val thy = ThyC.get_theory dI |
123 val ctxt = Proof_Context.init_global thy; |
123 val ctxt = Proof_Context.init_global thy; |
124 (*if*) mI = ["no_met"](*else*); |
124 (*if*) mI = ["no_met"](*else*); |
125 val pors = Problem.from_store ctxt pI |> #model |> O_Model.init thy fmz; |
125 val (pors, pctxt) = Problem.from_store ctxt pI |> #model |> O_Model.init_PIDE thy fmz; |
126 val pctxt = ContextC.initialise' thy fmz; |
|
127 val {cas, model, thy=thy',...} = Problem.from_store ctxt pI; (*take dI from _refined_ pbl*) |
126 val {cas, model, thy=thy',...} = Problem.from_store ctxt pI; (*take dI from _refined_ pbl*) |
128 "tracing bottom up"; Context.theory_name thy' = "Build_Inverse_Z_Transform"; (*WAS true*) |
127 "tracing bottom up"; Context.theory_name thy' = "Build_Inverse_Z_Transform"; (*WAS true*) |
129 val dI = Context.theory_name (ThyC.parent_of thy thy'); |
128 val dI = Context.theory_name (ThyC.parent_of thy thy'); |
130 "tracing bottom up"; dI = "Build_Inverse_Z_Transform"; (*WAS true*) |
129 "tracing bottom up"; dI = "Build_Inverse_Z_Transform"; (*WAS true*) |
131 cas = NONE; (*true*) |
130 cas = NONE; (*true*) |