test/Tools/isac/Minisubpbl/150a-add-given-Maximum.sml
changeset 60590 35846e25713e
parent 60588 9a116f94c5a6
child 60659 873f40b097bb
     1.1 --- a/test/Tools/isac/Minisubpbl/150a-add-given-Maximum.sml	Wed Nov 09 15:15:24 2022 +0100
     1.2 +++ b/test/Tools/isac/Minisubpbl/150a-add-given-Maximum.sml	Thu Nov 10 14:25:38 2022 +0100
     1.3 @@ -78,7 +78,7 @@
     1.4      val cmI = if mI = MethodC.id_empty then mI' else mI;
     1.5      val {model = pbt, where_rls, where_, ...} = Problem.from_store ctxt cpI;
     1.6      val {model = mpc, ...} = MethodC.from_store ctxt cmI
     1.7 -    val (preok, _) = Pre_Conds.check where_rls where_ pbl 0;
     1.8 +    val (preok, _) = Pre_Conds.check ctxt where_rls where_ pbl 0;
     1.9      (*if*) dI' = ThyC.id_empty andalso dI = ThyC.id_empty (*else*);
    1.10        (*if*) pI' = Problem.id_empty andalso pI = Problem.id_empty (*else*);
    1.11        (*case*) find_first (I_Model.is_error o #5) pbl (*of*);
    1.12 @@ -265,7 +265,7 @@
    1.13      val {origin = (root_model, _, _), ...} = Calc.specify_data (ctree, ([], Pos.Und))
    1.14      val (o_model', ctxt') = O_Model.complete_for m_patt root_model (o_model, ctxt)
    1.15      val thy = ThyC.get_theory_PIDE ctxt dI
    1.16 -    val (_, (i_model, _)) = M_Match.match_itms_oris thy i_prob (m_patt, where_, where_rls) o_model';
    1.17 +    val (_, (i_model, _)) = M_Match.match_itms_oris ctxt i_prob (m_patt, where_, where_rls) o_model';
    1.18  (*-------------------- stop step into me Specify_Problem -------------------------------------*)
    1.19  (*\\------------------ step into me Specify_Problem ----------------------------------------//*)
    1.20  
    1.21 @@ -308,7 +308,7 @@
    1.22    = (ctxt, oris, (o_refs, refs), (pbl, met));
    1.23      val cmI = if mI = MethodC.id_empty then mI' else mI;
    1.24      val {model = mpc, where_rls, where_, ...} = MethodC.from_store ctxt cmI;    (*..MethodC ?*)
    1.25 -    val (preok, _) = Pre_Conds.check where_rls where_ pbl 0;
    1.26 +    val (preok, _) = Pre_Conds.check ctxt where_rls where_ pbl 0;
    1.27  val NONE =
    1.28      (*case*) find_first (I_Model.is_error o #5) met (*of*);
    1.29