fun do_all (pt, (*old* )pos as( *old*) (p, _)) =

 fun do_all (pt, (p, _)) =

   let

   let

     val (o_model, o_refs as (_, _, met_id), ctxt) = case Ctree.get_obj I pt p of

     val (itms, oris, probl, o_refs, spec, ctxt) = case Ctree.get_obj I pt p of

       Ctree.PblObj {origin = (o_model, o_refs, _), ctxt, ...}

       Ctree.PblObj {meth = itms, origin = (oris, o_spec, _), probl, spec, ctxt, ...}

         => (o_model, o_refs, ctxt)

         => (itms, oris, probl, o_spec, spec, ctxt)

     | _ => raise ERROR "Specify.do_all: uncovered case get_obj"

     | _ => raise ERROR "LI.by_tactic: no PblObj"

     val mod_pat = MethodC.from_store ctxt met_id |> #model

     val (_, pbl_id', met_id') = References.select_input o_refs spec

     val i_model = map (I_Model.complete' mod_pat) o_model

     val {model = pbl_patt, ...} = Problem.from_store ctxt pbl_id';

       (*no parse, ^^^ takes existing terms; ctxt already created by O_Model.init*)

     val {model = met_patt, ...} = MethodC.from_store ctxt met_id';

     val (pt, _) = Ctree.cupdate_problem pt p (o_refs, i_model, i_model, ctxt)

     val (pbl_imod, met_imod) = I_Model.s_make_complete oris

       (I_Model.OLD_to_TEST probl, I_Model.OLD_to_TEST itms) (pbl_patt, met_patt)

     val (pt, _) = Ctree.cupdate_problem pt p

       (o_refs, I_Model.TEST_to_OLD pbl_imod, I_Model.TEST_to_OLD met_imod, ctxt)