18 val {cas, ppc, thy=thy',...} = get_pbt pI |
18 val {cas, ppc, thy=thy',...} = get_pbt pI |
19 val dI = theory2theory' (maxthy thy thy'); |
19 val dI = theory2theory' (maxthy thy thy'); |
20 val hdl = |
20 val hdl = |
21 case cas of SOME t => subst_atomic ((vars_of_pbl_' ppc) ~~~ vals_of_oris pors) t |
21 case cas of SOME t => subst_atomic ((vars_of_pbl_' ppc) ~~~ vals_of_oris pors) t |
22 | _ => error "Minisubplb/100-init-rootpbl.sml no headline" |
22 | _ => error "Minisubplb/100-init-rootpbl.sml no headline" |
23 val (pt, _) = cappend_problem e_ctree [] (e_istate, pctxt) (fmz, (dI, pI, mI)) |
23 val (pt, _) = cappend_problem e_ctree [] (Istate.empty, pctxt) (fmz, (dI, pI, mI)) |
24 (pors, (dI, pI, mI), hdl, ContextC.e_ctxt) |
24 (pors, (dI, pI, mI), hdl, ContextC.empty) |
25 ;((pt, ([], Pbl)), fst3 (Step_Specify.by_tactic_input Model_Problem (pt, ([], Pbl)))) : calcstate; |
25 ;((pt, ([], Pbl)), fst3 (Step_Specify.by_tactic_input Model_Problem (pt, ([], Pbl)))) : calcstate; |
26 |
26 |
27 (* INVESTIGATE val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];*) |
27 (* INVESTIGATE val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];*) |
28 (*///----------------------------------------- save for final check ------------------------\\\*) |
28 (*///----------------------------------------- save for final check ------------------------\\\*) |
29 val [(fmz''''', spec''''')] = [(fmz, (dI',pI',mI'))]; |
29 val [(fmz''''', spec''''')] = [(fmz, (dI',pI',mI'))]; |