1.1 --- a/src/Tools/isac/Interpret/calchead.sml Sat Jan 21 11:30:18 2017 +0100
1.2 +++ b/src/Tools/isac/Interpret/calchead.sml Sat Jan 21 12:01:30 2017 +0100
1.3 @@ -10,7 +10,7 @@
1.4 datatype appl = Appl of Ctree.tac_ | Notappl of string
1.5 val nxt_specify_init_calc : Selem.fmz -> calcstate
1.6 val specify : Ctree.tac_ -> Ctree.pos' -> Ctree.cid -> Ctree.ctree ->
1.7 - Ctree.pos' * (Ctree.pos' * Ctree.istate) * Generate.mout * Ctree.tac * Selem.safe * Ctree.ctree
1.8 + Ctree.pos' * (Ctree.pos' * Selem.istate) * Generate.mout * Ctree.tac * Selem.safe * Ctree.ctree
1.9 val nxt_specif : Ctree.tac -> Ctree.state -> calcstate'
1.10 val nxt_spec : Ctree.pos_ -> bool -> ori list -> spec -> itm list * itm list ->
1.11 (string * (term * 'a)) list * (string * (term * 'b)) list -> spec -> Ctree.pos_ * Ctree.tac
1.12 @@ -630,7 +630,7 @@
1.13 | "#Find" => Add_Find' (ct, met')
1.14 | "#Relate"=> Add_Relation'(ct, met')
1.15 | str => error ("specify_additem: uncovered case with " ^ str)
1.16 - val (p, Met, pt') = case Generate.generate1 thy arg (Uistate, ctxt) (p, Met) pt of
1.17 + val (p, Met, pt') = case Generate.generate1 thy arg (Selem.Uistate, ctxt) (p, Met) pt of
1.18 ((p, Met), _, _, pt') => (p, Met, pt')
1.19 | _ => error "specify_additem: uncovered case of generate1 (WARNING WHY ?)"
1.20 val pre' = check_preconds thy prls pre met'
1.21 @@ -638,7 +638,7 @@
1.22 val (p_, nxt) =
1.23 nxt_spec Met pb oris (dI',pI',mI') (pbl,met')
1.24 ((#ppc o Specify.get_pbt) cpI,ppc) (dI,pI,mI);
1.25 - in ((p, p_), ((p, p_), Uistate),
1.26 + in ((p, p_), ((p, p_), Selem.Uistate),
1.27 Generate.PpcKF (Generate.Method cmI, Specify.itms2itemppc thy met' pre'), nxt, Selem.Safe, pt')
1.28 end
1.29 | Err msg =>
1.30 @@ -648,7 +648,7 @@
1.31 val (p_, nxt) =
1.32 nxt_spec Met pb oris (dI',pI',mI') (pbl,met)
1.33 ((#ppc o Specify.get_pbt) cpI,(#ppc o Specify.get_met) cmI) (dI,pI,mI);
1.34 - in ((p,p_), ((p,p_),Uistate), Generate.Error' msg, nxt, Selem.Safe, pt) end
1.35 + in ((p,p_), ((p,p_),Selem.Uistate), Generate.Error' msg, nxt, Selem.Safe, pt) end
1.36 end
1.37 | specify_additem sel (ct, _) (p,_(*Frm, Pbl*)) _ pt =
1.38 let
1.39 @@ -670,14 +670,14 @@
1.40 | "#Find" => Add_Find' (ct, pbl')
1.41 | "#Relate"=> Add_Relation'(ct, pbl')
1.42 | str => error ("specify_additem Frm, Pbl: uncovered case with " ^ str)
1.43 - val ((p, Pbl), _, _, pt') = Generate.generate1 thy arg (Uistate, ctxt) (p,Pbl) pt (*WARNING SEE ABOVE*)
1.44 + val ((p, Pbl), _, _, pt') = Generate.generate1 thy arg (Selem.Uistate, ctxt) (p,Pbl) pt (*WARNING SEE ABOVE*)
1.45 val pre = check_preconds thy prls where_ pbl'
1.46 val pb = foldl and_ (true, map fst pre)
1.47 val (p_, nxt) =
1.48 nxt_spec Pbl pb oris (dI',pI',mI') (pbl',met) (ppc, (#ppc o Specify.get_met) cmI) (dI, pI, mI)
1.49 val ppc = if p_= Pbl then pbl' else met
1.50 in
1.51 - ((p, p_), ((p, p_), Uistate),
1.52 + ((p, p_), ((p, p_), Selem.Uistate),
1.53 Generate.PpcKF (header p_ pI cmI, Specify.itms2itemppc thy ppc pre), nxt, Selem.Safe, pt')
1.54 end
1.55 | Err msg =>
1.56 @@ -687,7 +687,7 @@
1.57 val (p_, nxt) =
1.58 nxt_spec Pbl pb oris (dI', pI', mI') (pbl, met)
1.59 (ppc, (#ppc o Specify.get_met) cmI) (dI, pI, mI)
1.60 - in ((p, p_), ((p, p_), Uistate), Generate.Error' msg, nxt, Selem.Safe,pt) end
1.61 + in ((p, p_), ((p, p_), Selem.Uistate), Generate.Error' msg, nxt, Selem.Safe,pt) end
1.62 end
1.63
1.64 fun specify (Init_Proof' (fmz, spec' as (dI', pI', mI'))) _ _ _ =
1.65 @@ -697,18 +697,18 @@
1.66 if dI' = e_domID orelse pI' = e_pblID (*andalso? WN110511*)
1.67 then ([], e_ctxt)
1.68 else pI' |> #ppc o Specify.get_pbt |> Specify.prep_ori fmz thy
1.69 - val (pt, _) = cappend_problem e_ctree [] (e_istate, ctxt) (fmz, spec')
1.70 + val (pt, _) = cappend_problem e_ctree [] (Selem.e_istate, ctxt) (fmz, spec')
1.71 (oris, (dI',pI',mI'), e_term)
1.72 val pt = update_ctxt pt [] ctxt
1.73 val (pbl, pre) = ([], [])
1.74 in
1.75 case mI' of
1.76 ["no_met"] =>
1.77 - (([], Pbl), (([], Pbl), Uistate),
1.78 + (([], Pbl), (([], Pbl), Selem.Uistate),
1.79 Generate.PpcKF (Generate.Problem [], Specify.itms2itemppc (assoc_thy dI') pbl pre),
1.80 Refine_Tacitly pI', Selem.Safe, pt)
1.81 | _ =>
1.82 - (([], Pbl), (([], Pbl), Uistate),
1.83 + (([], Pbl), (([], Pbl), Selem.Uistate),
1.84 Generate.PpcKF (Generate.Problem [], Specify.itms2itemppc (assoc_thy dI') pbl pre),
1.85 Model_Problem, Selem.Safe, pt)
1.86 end
1.87 @@ -725,11 +725,11 @@
1.88 val pre = check_preconds thy prls where_ pbl
1.89 val pb = foldl and_ (true, map fst pre)
1.90 val ((p, _), _, _, pt) =
1.91 - Generate.generate1 thy (Model_Problem'([],pbl,met)) (Uistate, ctxt) pos pt
1.92 + Generate.generate1 thy (Model_Problem'([],pbl,met)) (Selem.Uistate, ctxt) pos pt
1.93 val (_, nxt) = nxt_spec Pbl pb oris (dI', pI', mI') (pbl, met)
1.94 (ppc,(#ppc o Specify.get_met) mI') (dI',pI',mI');
1.95 in
1.96 - ((p, Pbl), ((p, p_), Uistate),
1.97 + ((p, Pbl), ((p, p_), Selem.Uistate),
1.98 Generate.PpcKF (Generate.Problem pI', Specify.itms2itemppc (assoc_thy dI') pbl pre),
1.99 nxt, Selem.Safe, pt)
1.100 end
1.101 @@ -742,9 +742,9 @@
1.102 val {met, thy,...} = Specify.get_pbt pIre
1.103 val (domID, metID) = (string_of_thy thy, if length met = 0 then e_metID else hd met)
1.104 val ((p,_), _, _, pt) =
1.105 - Generate.generate1 thy (Refine_Tacitly' (pI, pIre, domID, metID, [(*pbl*)])) (Uistate, ctxt) pos pt
1.106 + Generate.generate1 thy (Refine_Tacitly' (pI, pIre, domID, metID, [(*pbl*)])) (Selem.Uistate, ctxt) pos pt
1.107 val (pbl, pre, _) = ([], [], false)
1.108 - in ((p, Pbl), (pos, Uistate),
1.109 + in ((p, Pbl), (pos, Selem.Uistate),
1.110 Generate.PpcKF (Generate.Problem pIre, Specify.itms2itemppc (assoc_thy dI') pbl pre),
1.111 Model_Problem, Selem.Safe, pt)
1.112 end
1.113 @@ -752,9 +752,9 @@
1.114 let
1.115 val ctxt = get_ctxt pt pos
1.116 val (pos, _, _, pt) =
1.117 - Generate.generate1 (assoc_thy "Isac") (Refine_Problem' rfd) (Uistate, ctxt) pos pt
1.118 + Generate.generate1 (assoc_thy "Isac") (Refine_Problem' rfd) (Selem.Uistate, ctxt) pos pt
1.119 in
1.120 - (pos(*p,Pbl*), (pos(*p,Pbl*), Uistate), Generate.RefinedKF rfd, Model_Problem, Selem.Safe, pt)
1.121 + (pos(*p,Pbl*), (pos(*p,Pbl*), Selem.Uistate), Generate.RefinedKF rfd, Model_Problem, Selem.Safe, pt)
1.122 end
1.123 (*WN110515 initialise ctxt again from itms and add preconds*)
1.124 | specify (Specify_Problem' (pI, (ok, (itms, pre)))) (pos as (p,_)) _ pt =
1.125 @@ -765,7 +765,7 @@
1.126 | _ => error "specify (Specify_Problem': uncovered case get_obj"
1.127 val thy = assoc_thy dI
1.128 val (p, Pbl, pt) =
1.129 - case Generate.generate1 thy (Specify_Problem' (pI, (ok, (itms, pre)))) (Uistate, ctxt) pos pt of
1.130 + case Generate.generate1 thy (Specify_Problem' (pI, (ok, (itms, pre)))) (Selem.Uistate, ctxt) pos pt of
1.131 ((p, Pbl), _, _, pt) => (p, Pbl, pt)
1.132 | _ => error "specify (Specify_Problem': uncovered case generate1 (WARNING WHY ?)"
1.133 val dI'' = assoc_thy (if dI=e_domID then dI' else dI)
1.134 @@ -773,7 +773,7 @@
1.135 val (_, nxt) = nxt_spec Pbl ok oris (dI', pI', mI') (itms, met) ((#ppc o Specify.get_pbt) pI,
1.136 (#ppc o Specify.get_met) mI'') (dI, pI, mI);
1.137 in
1.138 - ((p,Pbl), (pos,Uistate),
1.139 + ((p,Pbl), (pos,Selem.Uistate),
1.140 Generate.PpcKF (Generate.Problem pI, Specify.itms2itemppc dI'' itms pre),
1.141 nxt, Selem.Safe, pt)
1.142 end
1.143 @@ -792,11 +792,11 @@
1.144 val met = if met = [] then pbl else met
1.145 val (_, (itms, pre')) = Specify.match_itms_oris thy met (ppc, pre, prls ) oris
1.146 val (pos, _, _, pt) =
1.147 - Generate.generate1 thy (Specify_Method' (mID, oris, itms)) (Uistate, ctxt) pos pt
1.148 + Generate.generate1 thy (Specify_Method' (mID, oris, itms)) (Selem.Uistate, ctxt) pos pt
1.149 val (_, nxt) = nxt_spec Met true oris (dI', pI',mI') (pbl, itms)
1.150 ((#ppc o Specify.get_pbt) pI'', ppc) (dI'', pI'', mID)
1.151 in
1.152 - (pos, (pos,Uistate),
1.153 + (pos, (pos,Selem.Uistate),
1.154 Generate.PpcKF (Generate.Method mID, Specify.itms2itemppc (assoc_thy dI'') itms pre'),
1.155 nxt, Selem.Safe, pt)
1.156 end
1.157 @@ -825,16 +825,16 @@
1.158 then
1.159 let val (p_, nxt) = nxt_spec p_ pb oris (dI', pI', mI') (pbl, met) (ppc, mpc) (dI, pI, mI)
1.160 in
1.161 - ((p, p_), (pos, Uistate),
1.162 + ((p, p_), (pos, Selem.Uistate),
1.163 Generate.PpcKF (header p_ pI cmI, Specify.itms2itemppc thy mppc pre),
1.164 nxt, Selem.Safe, pt)
1.165 end
1.166 else (*FIXME: check ppc wrt. (new!) domID ..? still parsable?*)
1.167 let
1.168 - val ((p, p_), _, _, pt) = Generate.generate1 thy (Specify_Theory' domID) (Uistate, ctxt) (p,p_) pt
1.169 + val ((p, p_), _, _, pt) = Generate.generate1 thy (Specify_Theory' domID) (Selem.Uistate, ctxt) (p,p_) pt
1.170 val (p_,nxt) = nxt_spec p_ pb oris (dI', pI', mI') (pbl, met) (ppc, mpc) (domID, pI, mI)
1.171 in
1.172 - ((p,p_), (pos,Uistate),
1.173 + ((p,p_), (pos,Selem.Uistate),
1.174 Generate.PpcKF (header p_ pI cmI, Specify.itms2itemppc thy mppc pre),
1.175 nxt, Selem.Safe, pt)
1.176 end
1.177 @@ -861,16 +861,16 @@
1.178 | "#Find" => (Add_Find ct, Add_Find' (ct, pbl'))
1.179 | "#Relate"=> (Add_Relation ct, Add_Relation'(ct, pbl'))
1.180 | sel => error ("nxt_specif_additem: uncovered case of" ^ sel)
1.181 - val (p, Pbl, c, pt') = case Generate.generate1 thy tac_ (Uistate, ctxt) (p,Pbl) pt of
1.182 + val (p, Pbl, c, pt') = case Generate.generate1 thy tac_ (Selem.Uistate, ctxt) (p,Pbl) pt of
1.183 ((p, Pbl), c, _, pt') => (p, Pbl, c, pt')
1.184 | _ => error "nxt_specif_additem: uncovered case generate1 (WARNING WHY ?)"
1.185 in
1.186 - ([(tac, tac_, ((p, Pbl), (Uistate, ctxt)))], c, (pt', (p, Pbl))) : calcstate'
1.187 + ([(tac, tac_, ((p, Pbl), (Selem.Uistate, ctxt)))], c, (pt', (p, Pbl))) : calcstate'
1.188 end
1.189 | Err msg => (*TODO.WN03 pass error-msgs to the frontend..
1.190 FIXME ..and dont abuse a tactic for that purpose*)
1.191 ([(Tac msg, Tac_ (Thy_Info.get_theory "Pure", msg,msg,msg),
1.192 - (e_pos', (e_istate, e_ctxt)))], [], ptp)
1.193 + (e_pos', (Selem.e_istate, e_ctxt)))], [], ptp)
1.194 end
1.195 | nxt_specif_additem sel ct (ptp as (pt, (p, Met))) =
1.196 let
1.197 @@ -890,11 +890,11 @@
1.198 | "#Find" => (Add_Find ct, Add_Find' (ct, met'))
1.199 | "#Relate"=> (Add_Relation ct, Add_Relation'(ct, met'))
1.200 | sel => error ("nxt_specif_additem Met: uncovered case of" ^ sel)
1.201 - val (p, Met, c, pt') = case Generate.generate1 thy tac_ (Uistate, ctxt) (p, Met) pt of
1.202 + val (p, Met, c, pt') = case Generate.generate1 thy tac_ (Selem.Uistate, ctxt) (p, Met) pt of
1.203 ((p, Met), c, _, pt') => (p, Met, c, pt')
1.204 | _ => error "nxt_specif_additem: uncovered case generate1 (WARNING WHY ?)"
1.205 in
1.206 - ([(tac, tac_, ((p, Met), (Uistate, ctxt)))], c, (pt', (p, Met)))
1.207 + ([(tac, tac_, ((p, Met), (Selem.Uistate, ctxt)))], c, (pt', (p, Met)))
1.208 end
1.209 | Err _ => ([(*tacis*)], [], ptp) (*nxt_me collects tacis until not hide; here just no progress*)
1.210 end
1.211 @@ -973,8 +973,8 @@
1.212 | _ => complete_mod_ (oris, mpc, ppc, probl)
1.213 (*----------------------------------------------------------------*)
1.214 val tac_ = Model_Problem' (pI, pbl, met)
1.215 - val (pos,c,_,pt) = Generate.generate1 thy tac_ (Uistate, ctxt) pos pt
1.216 - in ([(tac, tac_, (pos, (Uistate, e_ctxt)))], c, (pt,pos)) : calcstate' end
1.217 + val (pos,c,_,pt) = Generate.generate1 thy tac_ (Selem.Uistate, ctxt) pos pt
1.218 + in ([(tac, tac_, (pos, (Selem.Uistate, e_ctxt)))], c, (pt,pos)) : calcstate' end
1.219 | nxt_specif (Add_Given ct) ptp = nxt_specif_additem "#Given" ct ptp
1.220 | nxt_specif (Add_Find ct) ptp = nxt_specif_additem "#Find" ct ptp
1.221 | nxt_specif (Add_Relation ct) ptp = nxt_specif_additem"#Relate" ct ptp
1.222 @@ -994,10 +994,10 @@
1.223 val mI = if length met = 0 then e_metID else hd met
1.224 val thy = assoc_thy dI
1.225 val (pos, c, _, pt) =
1.226 - Generate.generate1 thy (Refine_Tacitly' (pI, pI', dI, mI,(*pbl*)[])) (Uistate, ctxt) pos pt
1.227 + Generate.generate1 thy (Refine_Tacitly' (pI, pI', dI, mI,(*pbl*)[])) (Selem.Uistate, ctxt) pos pt
1.228 in
1.229 ([(Refine_Tacitly pI, Refine_Tacitly' (pI,pI',dI,mI,(*pbl*)[]),
1.230 - (pos, (Uistate, e_ctxt)))], c, (pt,pos))
1.231 + (pos, (Selem.Uistate, e_ctxt)))], c, (pt,pos))
1.232 end
1.233 | NONE => ([], [], ptp)
1.234 end
1.235 @@ -1013,9 +1013,9 @@
1.236 NONE => ([], [], ptp)
1.237 | SOME rfd =>
1.238 let
1.239 - val (pos,c,_,pt) = Generate.generate1 (assoc_thy thy) (Refine_Problem' rfd) (Uistate, ctxt) pos pt
1.240 + val (pos,c,_,pt) = Generate.generate1 (assoc_thy thy) (Refine_Problem' rfd) (Selem.Uistate, ctxt) pos pt
1.241 in
1.242 - ([(Refine_Problem pI, Refine_Problem' rfd, (pos, (Uistate, e_ctxt)))], c, (pt,pos))
1.243 + ([(Refine_Problem pI, Refine_Problem' rfd, (pos, (Selem.Uistate, e_ctxt)))], c, (pt,pos))
1.244 end
1.245 end
1.246 | nxt_specif (Specify_Problem pI) (pt, pos as (p,_)) =
1.247 @@ -1031,11 +1031,11 @@
1.248 then (false, (Generate.init_pbl ppc, []))
1.249 else Specify.match_itms_oris thy probl (ppc,where_,prls) oris
1.250 (*FIXXXME~~~~~~~~~~~~~~~: take pbl and compare with new pI WN.8.03*)
1.251 - val (c, pt) = case Generate.generate1 thy (Specify_Problem' (pI, pbl)) (Uistate, ctxt) pos pt of
1.252 + val (c, pt) = case Generate.generate1 thy (Specify_Problem' (pI, pbl)) (Selem.Uistate, ctxt) pos pt of
1.253 ((_, Pbl), c, _, pt) => (c, pt)
1.254 | _ => error ""
1.255 in
1.256 - ([(Specify_Problem pI, Specify_Problem' (pI, pbl), (pos, (Uistate, e_ctxt)))], c, (pt,pos))
1.257 + ([(Specify_Problem pI, Specify_Problem' (pI, pbl), (pos, (Selem.Uistate, e_ctxt)))], c, (pt,pos))
1.258 end
1.259 (* transfers oris (not required in pbl) to met-model for script-env
1.260 FIXME.WN.8.03: application of several mIDs to SAME model? *)
1.261 @@ -1051,25 +1051,25 @@
1.262 val met = if met=[] then pbl else met (* WN0602 what if more itms in met? *)
1.263 val (_, (itms, _)) = Specify.match_itms_oris thy met (ppc,pre,prls ) oris
1.264 val (pos, c, _, pt) =
1.265 - Generate.generate1 thy (Specify_Method' (mID, oris, itms)) (Uistate, ctxt) pos pt
1.266 + Generate.generate1 thy (Specify_Method' (mID, oris, itms)) (Selem.Uistate, ctxt) pos pt
1.267 in
1.268 - ([(Specify_Method mID, Specify_Method' (mID, oris, itms), (pos, (Uistate, e_ctxt)))], c, (pt, pos))
1.269 + ([(Specify_Method mID, Specify_Method' (mID, oris, itms), (pos, (Selem.Uistate, e_ctxt)))], c, (pt, pos))
1.270 end
1.271 | nxt_specif (Specify_Theory dI) (pt, pos as (_, Pbl)) =
1.272 let
1.273 val ctxt = get_ctxt pt pos
1.274 val (pos, c, _, pt) =
1.275 - Generate.generate1 (assoc_thy "Isac") (Specify_Theory' dI) (Uistate, ctxt) pos pt
1.276 + Generate.generate1 (assoc_thy "Isac") (Specify_Theory' dI) (Selem.Uistate, ctxt) pos pt
1.277 in (*FIXXXME: check if pbl can still be parsed*)
1.278 - ([(Specify_Theory dI, Specify_Theory' dI, (pos, (Uistate, ctxt)))], c,
1.279 + ([(Specify_Theory dI, Specify_Theory' dI, (pos, (Selem.Uistate, ctxt)))], c,
1.280 (pt, pos))
1.281 end
1.282 | nxt_specif (Specify_Theory dI) (pt, pos as (_, Met)) =
1.283 let
1.284 val ctxt = get_ctxt pt pos
1.285 - val (pos, c, _, pt) = Generate.generate1 (assoc_thy "Isac") (Specify_Theory' dI) (Uistate, ctxt) pos pt
1.286 + val (pos, c, _, pt) = Generate.generate1 (assoc_thy "Isac") (Specify_Theory' dI) (Selem.Uistate, ctxt) pos pt
1.287 in (*FIXXXME: check if met can still be parsed*)
1.288 - ([(Specify_Theory dI, Specify_Theory' dI, (pos, (Uistate, ctxt)))], c, (pt, pos))
1.289 + ([(Specify_Theory dI, Specify_Theory' dI, (pos, (Selem.Uistate, ctxt)))], c, (pt, pos))
1.290 end
1.291 | nxt_specif m' _ = error ("nxt_specif: not impl. for "^tac2str m')
1.292
1.293 @@ -1087,7 +1087,7 @@
1.294 val dI = if dI = "" then theory2theory' thy else dI
1.295 val mI = if mI = [] then hd met else mI
1.296 val hdl = case cas of NONE => pblterm dI pI | SOME t => t
1.297 - val (pt,_) = cappend_problem e_ctree [] (Uistate, e_ctxt) ([], (dI, pI, mI))
1.298 + val (pt,_) = cappend_problem e_ctree [] (Selem.Uistate, e_ctxt) ([], (dI, pI, mI))
1.299 ([], (dI,pI,mI), hdl)
1.300 val pt = update_spec pt [] (dI, pI, mI)
1.301 val pits = Generate.init_pbl' ppc
1.302 @@ -1100,7 +1100,7 @@
1.303 val {ppc, ...} = Specify.get_met mI
1.304 val dI = if dI = "" then "Isac" else dI
1.305 val (pt, _) =
1.306 - cappend_problem e_ctree [] (e_istate, e_ctxt) ([], (dI, pI, mI)) ([], (dI, pI, mI), e_term (*FIXME met*))
1.307 + cappend_problem e_ctree [] (Selem.e_istate, e_ctxt) ([], (dI, pI, mI)) ([], (dI, pI, mI), e_term (*FIXME met*))
1.308 val pt = update_spec pt [] (dI, pI, mI)
1.309 val mits = Generate.init_pbl' ppc
1.310 val pt = update_met pt [] mits
1.311 @@ -1108,7 +1108,7 @@
1.312 else (* new example, pepare for interactive modeling *)
1.313 let
1.314 val (pt, _) =
1.315 - cappend_problem e_ctree [] (e_istate, e_ctxt) ([], e_spec) ([], e_spec, e_term)
1.316 + cappend_problem e_ctree [] (Selem.e_istate, e_ctxt) ([], e_spec) ([], e_spec, e_term)
1.317 in ((pt, ([], Pbl)), []) end
1.318 | nxt_specify_init_calc (fmz, (dI, pI, mI)) =
1.319 let (* both """"""""""""""""""""""""" either empty or complete *)
1.320 @@ -1129,7 +1129,7 @@
1.321 NONE => pblterm dI pI
1.322 | SOME t => subst_atomic ((vars_of_pbl_' ppc) ~~~ vals_of_oris pors) t
1.323 val (pt, _) =
1.324 - cappend_problem e_ctree [] (e_istate, pctxt) (fmz, (dI, pI, mI)) (pors, (dI, pI, mI), hdl)
1.325 + cappend_problem e_ctree [] (Selem.e_istate, pctxt) (fmz, (dI, pI, mI)) (pors, (dI, pI, mI), hdl)
1.326 val pt = update_ctxt pt [] pctxt
1.327 in
1.328 ((pt, ([], Pbl)), fst3 (nxt_specif Model_Problem (pt, ([], Pbl)))) : calcstate