1.1 --- a/test/Tools/isac/Minisubpbl/150a-add-given-Maximum.sml	Wed Sep 27 12:17:44 2023 +0200
     1.2 +++ b/test/Tools/isac/Minisubpbl/150a-add-given-Maximum.sml	Mon Oct 02 12:02:59 2023 +0200
     1.3 @@ -420,18 +420,11 @@
     1.4            (*if*) Ctree.is_pblobj ppobj (*then*);
     1.5  
     1.6             pt_model ppobj p_;
     1.7 -"~~~~~ fun pt_model , args:"; val ((Ctree.PblObj {probl, spec, origin = (_, spec', hdl), ctxt, ...}), 
     1.8 +"~~~~~ fun pt_model , args:"; val ((Ctree.PblObj {probl, spec, origin = (_, o_spec, hdl), ctxt, ...}), 
     1.9    Pbl(*Frm,Pbl*)) = (ppobj, p_);
    1.10 -      val (_, pI, _) = Ctree.get_somespec' spec spec';
    1.11 -                 (*if*) pI = Problem.id_empty (*else*); 
    1.12 -(*    val where_ = if pI = Problem.id_empty then []*)
    1.13 -(*      else                                       *)
    1.14 -(*        let                                      *)
    1.15 -	          val {where_rls, where_, model, ...} = Problem.from_store ctxt pI
    1.16 -	          val (_, where_) = (*Pre_Conds.*)check ctxt where_rls where_ (model, I_Model.OLD_to_TEST probl)
    1.17 -(*        in where_ end                           *)
    1.18 -	    val allcorrect = I_Model.is_complete probl andalso foldl and_ (true, (map #1 where_))
    1.19 -val return_pt_model = Ctree.ModSpec (allcorrect, Pos.Pbl, hdl, probl, where_, spec)
    1.20 +      val (_, _, met_id) = References.select_input o_spec spec
    1.21 +      val (allcorr, _) = Pre_Conds.check_internal ctxt (I_Model.OLD_to_TEST probl) (Pos.Met, met_id)
    1.22 +val return_pt_model = Ctree.ModSpec (allcorr, Pos.Pbl, hdl, probl, (*where_*)[(*Problem.from_store in check*)], spec)
    1.23  
    1.24  (*|------------------- continue with TESTg_form ----------------------------------------------*)
    1.25  val Ctree.ModSpec (spec as (_, p_, _, gfr, where_, _)) =