184 else O_Model.init thy fmz_ pbt |> #1; |
184 else O_Model.init thy fmz_ pbt |> #1; |
185 in (Pos.Pbl, appl_adds dI' oris probl pbt |
185 in (Pos.Pbl, appl_adds dI' oris probl pbt |
186 (map (itms2fstr ctxt) probl), meth) end |
186 (map (itms2fstr ctxt) probl), meth) end |
187 else if mI <> smI (*FIXME.WN0311: what if probl is incomplete?!*) |
187 else if mI <> smI (*FIXME.WN0311: what if probl is incomplete?!*) |
188 then let |
188 then let |
189 (*OLD* ) |
|
190 val met = (#model o MethodC.from_store ctxt) mI |
|
191 val mits = I_Model.complete oris probl meth met |
|
192 in if foldl and_ (true, map #3 mits) |
|
193 then (Pos.Pbl, probl, mits) else (Pos.Met, probl, mits) |
|
194 ( *---*) |
|
195 val pbl_patt = (#model o Problem.from_store ctxt) pI |
189 val pbl_patt = (#model o Problem.from_store ctxt) pI |
196 val met = (#model o MethodC.from_store ctxt) mI |
190 val met = (#model o MethodC.from_store ctxt) mI |
197 val (_, mits) = I_Model.s_make_complete oris |
191 val (_, mits) = I_Model.s_make_complete oris |
198 (I_Model.OLD_to_TEST probl, I_Model.OLD_to_TEST meth) (met, pbl_patt) |
192 (I_Model.OLD_to_TEST probl, I_Model.OLD_to_TEST meth) (met, pbl_patt) |
199 in if foldl and_ (true, map #3 mits) |
193 in if foldl and_ (true, map #3 mits) |
200 then (Pos.Pbl, probl, I_Model.TEST_to_OLD mits) |
194 then (Pos.Pbl, probl, I_Model.TEST_to_OLD mits) |
201 else (Pos.Met, probl, I_Model.TEST_to_OLD mits) |
195 else (Pos.Met, probl, I_Model.TEST_to_OLD mits) |
202 (*NEW*) |
|
203 end |
196 end |
204 else (Pos.Pbl, appl_adds (#1 (References.select_input ospec spec)) oris [(*!!!*)] |
197 else (Pos.Pbl, appl_adds (#1 (References.select_input ospec spec)) oris [(*!!!*)] |
205 ((#model o Problem.from_store ctxt) |
198 ((#model o Problem.from_store ctxt) |
206 (#2 (References.select_input ospec spec))) |
199 (#2 (References.select_input ospec spec))) |
207 (imodel2fstr imodel), meth) |
200 (imodel2fstr imodel), meth) |