183 if pI = #2 ospec then oris |
183 if pI = #2 ospec then oris |
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 val met = (#model o MethodC.from_store ctxt) mI |
188 then let |
|
189 (*OLD* ) |
|
190 val met = (#model o MethodC.from_store ctxt) mI |
189 val mits = I_Model.complete oris probl meth met |
191 val mits = I_Model.complete oris probl meth met |
190 in if foldl and_ (true, map #3 mits) |
192 in if foldl and_ (true, map #3 mits) |
191 then (Pos.Pbl, probl, mits) else (Pos.Met, probl, mits) |
193 then (Pos.Pbl, probl, mits) else (Pos.Met, probl, mits) |
|
194 ( *---*) |
|
195 val pbl_patt = (#model o Problem.from_store ctxt) pI |
|
196 val met = (#model o MethodC.from_store ctxt) mI |
|
197 val (_, mits) = I_Model.s_make_complete oris |
|
198 (I_Model.OLD_to_TEST probl, I_Model.OLD_to_TEST meth) (met, pbl_patt) |
|
199 in if foldl and_ (true, map #3 mits) |
|
200 then (Pos.Pbl, probl, I_Model.TEST_to_OLD mits) |
|
201 else (Pos.Met, probl, I_Model.TEST_to_OLD mits) |
|
202 (*NEW*) |
192 end |
203 end |
193 else (Pos.Pbl, appl_adds (#1 (References.select_input ospec spec)) oris [(*!!!*)] |
204 else (Pos.Pbl, appl_adds (#1 (References.select_input ospec spec)) oris [(*!!!*)] |
194 ((#model o Problem.from_store ctxt) |
205 ((#model o Problem.from_store ctxt) |
195 (#2 (References.select_input ospec spec))) |
206 (#2 (References.select_input ospec spec))) |
196 (imodel2fstr imodel), meth) |
207 (imodel2fstr imodel), meth) |