406 val ("dummy", (Pbl, Refine_Problem ["sqroot-test", "univariate", "equation", "test"])) = |
406 val ("dummy", (Pbl, Refine_Problem ["sqroot-test", "univariate", "equation", "test"])) = |
407 for_problem oris (o_refs, refs) (pbl, met); |
407 for_problem oris (o_refs, refs) (pbl, met); |
408 "~~~~~ fun for_problem , args:"; val (oris, ((dI', pI', mI'), (dI, pI, mI)), (pbl, met)) = |
408 "~~~~~ fun for_problem , args:"; val (oris, ((dI', pI', mI'), (dI, pI, mI)), (pbl, met)) = |
409 (oris, (o_refs, refs), (pbl, met)); |
409 (oris, (o_refs, refs), (pbl, met)); |
410 val cpI = if pI = Problem.id_empty then pI' else pI; |
410 val cpI = if pI = Problem.id_empty then pI' else pI; |
411 val cmI = if mI = Method.id_empty then mI' else mI; |
411 val cmI = if mI = MethodC.id_empty then mI' else mI; |
412 val {ppc = pbt, prls, where_, ...} = Problem.from_store cpI; |
412 val {ppc = pbt, prls, where_, ...} = Problem.from_store cpI; |
413 val {ppc = mpc, ...} = Method.from_store cmI |
413 val {ppc = mpc, ...} = MethodC.from_store cmI |
414 val (preok, (*+*)xxxxx(*+*) ) = Pre_Conds.check prls where_ pbl 0; |
414 val (preok, (*+*)xxxxx(*+*) ) = Pre_Conds.check prls where_ pbl 0; |
415 (*if*) dI' = ThyC.id_empty andalso dI = ThyC.id_empty (*else*); |
415 (*if*) dI' = ThyC.id_empty andalso dI = ThyC.id_empty (*else*); |
416 (*if*) pI' = Problem.id_empty andalso pI = Problem.id_empty (*else*); |
416 (*if*) pI' = Problem.id_empty andalso pI = Problem.id_empty (*else*); |
417 val NONE = (*case*) find_first (I_Model.is_error o #5) pbl (*of*); |
417 val NONE = (*case*) find_first (I_Model.is_error o #5) pbl (*of*); |
418 val NONE = (*case*) |
418 val NONE = (*case*) |