55 case Ctree.get_obj I pt p of |
55 case Ctree.get_obj I pt p of |
56 pblobj as (Ctree.PblObj {meth, origin = origin as (oris, (dI', pI', mI'), _), |
56 pblobj as (Ctree.PblObj {meth, origin = origin as (oris, (dI', pI', mI'), _), |
57 probl, spec = (dI, pI, mI), ...}) => (pblobj, meth, origin, oris, dI', pI', mI', probl, dI, pI, mI) |
57 probl, spec = (dI, pI, mI), ...}) => (pblobj, meth, origin, oris, dI', pI', mI', probl, dI, pI, mI) |
58 | Ctree.PrfObj _ => error "nxt_specify_: not on PrfObj"; |
58 | Ctree.PrfObj _ => error "nxt_specify_: not on PrfObj"; |
59 (*if*) Ctree.just_created_ pblobj (*by Subproblem*) andalso origin <> Ctree.e_origin (*else*); |
59 (*if*) Ctree.just_created_ pblobj (*by Subproblem*) andalso origin <> Ctree.e_origin (*else*); |
60 val cpI = if pI = Celem.e_pblID then pI' else pI; |
60 val cpI = if pI = Spec.e_pblID then pI' else pI; |
61 val cmI = if mI = Celem.e_metID then mI' else mI; |
61 val cmI = if mI = Spec.e_metID then mI' else mI; |
62 val {ppc, prls, where_, ...} = Specify.get_pbt cpI; |
62 val {ppc, prls, where_, ...} = Specify.get_pbt cpI; |
63 val pre = Stool.check_preconds "thy 100820" prls where_ probl; |
63 val pre = Stool.check_preconds "thy 100820" prls where_ probl; |
64 val pb = foldl and_ (true, map fst pre); |
64 val pb = foldl and_ (true, map fst pre); |
65 |
65 |
66 val (Pbl, Specify_Theory "Integrate") = |
66 val (Pbl, Specify_Theory "Integrate") = |
67 Chead.nxt_spec p_ pb oris (dI', pI', mI') (probl, meth) (ppc, (#ppc o Specify.get_met) cmI) (dI, pI, mI); |
67 Chead.nxt_spec p_ pb oris (dI', pI', mI') (probl, meth) (ppc, (#ppc o Specify.get_met) cmI) (dI, pI, mI); |
68 "~~~~~ fun nxt_spec , args:"; val (Pbl, preok, oris, (dI', pI', mI'), (pbl, met), (pbt, mpc), (dI, pI, mI)) |
68 "~~~~~ fun nxt_spec , args:"; val (Pbl, preok, oris, (dI', pI', mI'), (pbl, met), (pbt, mpc), (dI, pI, mI)) |
69 (* vv----^^*) |
69 (* vv----^^*) |
70 = (p_, pb, oris, (dI', pI', mI'), (probl, meth), (ppc, (#ppc o Specify.get_met) cmI), (dI, pI, mI)); |
70 = (p_, pb, oris, (dI', pI', mI'), (probl, meth), (ppc, (#ppc o Specify.get_met) cmI), (dI, pI, mI)); |
71 (*if*) dI' = ThyC.id_empty andalso dI = ThyC.id_empty (*else*); |
71 (*if*) dI' = ThyC.id_empty andalso dI = ThyC.id_empty (*else*); |
72 (*if*) pI' = Celem.e_pblID andalso pI = Celem.e_pblID (*else*); |
72 (*if*) pI' = Spec.e_pblID andalso pI = Spec.e_pblID (*else*); |
73 val NONE = (*case*) find_first (is_error o #5) pbl (*of*); |
73 val NONE = (*case*) find_first (is_error o #5) pbl (*of*); |
74 val NONE = (*case*) nxt_add (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) oris pbt pbl (*of*); |
74 val NONE = (*case*) nxt_add (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) oris pbt pbl (*of*); |
75 (*if*) not preok (*else*); |
75 (*if*) not preok (*else*); |
76 (*if*) dI = ThyC.id_empty (*then*); |
76 (*if*) dI = ThyC.id_empty (*then*); |
77 |
77 |