1.1 --- a/src/Tools/isac/Specify/specification.sml	Wed Sep 27 12:17:44 2023 +0200
     1.2 +++ b/src/Tools/isac/Specify/specification.sml	Mon Oct 02 12:02:59 2023 +0200
     1.3 @@ -91,17 +91,17 @@
     1.4    foldl and_ (true, map #1 (where_: Pre_Conds.T)) andalso 
     1.5    dI <> ThyC.id_empty andalso pI <> Problem.id_empty andalso mI <> MethodC.id_empty
     1.6  
     1.7 -(* check I_Model.is_complete either for Problem or MethodC *)
     1.8 -fun is_complete (pt, pos as (p, Pos.Pbl)) =
     1.9 -    if (Ctree.is_pblobj o (Ctree.get_obj I pt)) p 
    1.10 -    then (I_Model.is_complete o (Ctree.get_obj Ctree.g_pbl pt)) p
    1.11 -    else raise ERROR ("is_complete: called by PrfObj at " ^ Pos.pos'2str pos)
    1.12 -  | is_complete (pt, pos as (p, Pos.Met)) = 
    1.13 -    if (Ctree.is_pblobj o (Ctree.get_obj I pt)) p 
    1.14 -    then (I_Model.is_complete o (Ctree.get_obj Ctree.g_met pt)) p
    1.15 -    else raise ERROR ("is_complete: called by PrfObj at " ^ Pos.pos'2str pos)
    1.16 -  | is_complete (_, pos) =
    1.17 -    raise ERROR ("is_complete called by " ^ Pos.pos'2str pos ^ " (should be Pbl or Met)")
    1.18 +fun is_complete (pt, (p, _)) =
    1.19 +  let
    1.20 +    val (itms, oris, probl, o_spec, spec, ctxt) = case Ctree.get_obj I pt p of
    1.21 +       Ctree.PblObj {meth = itms, origin = (oris, o_spec, _), probl, spec, ctxt, ...}
    1.22 +       => (itms, oris, probl, o_spec, spec, ctxt)
    1.23 +    | _ => raise ERROR "SpecificationC.is_complete only with PblObj"
    1.24 +    val (_, pbl_id, met_id) = References.select_input o_spec spec
    1.25 +  in
    1.26 +    I_Model.s_are_complete ctxt oris
    1.27 +        (I_Model.OLD_to_TEST probl, I_Model.OLD_to_TEST itms) (pbl_id, met_id)
    1.28 +  end
    1.29  
    1.30  (** handle acces to Ctree **)
    1.31