1.1 --- a/test/Tools/isac/Minisubpbl/150a-add-given-Maximum.sml	Mon Oct 02 15:39:22 2023 +0200
     1.2 +++ b/test/Tools/isac/Minisubpbl/150a-add-given-Maximum.sml	Tue Oct 03 16:31:59 2023 +0200
     1.3 @@ -74,9 +74,9 @@
     1.4                (model, I_Model.OLD_to_TEST probl);
     1.5  "~~~~~ fun check , args:"; val (ctxt, where_rls, pres, (model_patt, i_model)) =
     1.6    (ctxt, where_rls, where_, (model, I_Model.OLD_to_TEST probl));
     1.7 -      val (_, _, (env_subst, env_eval)) =
     1.8 -           of_max_variant model_patt i_model;
     1.9 -"~~~~~ fun of_max_variant , args:"; val (_, []) = (model_patt, i_model);
    1.10 +      val (env_model, (env_subst, env_eval)) = 
    1.11 +           make_environments model_patt i_model;
    1.12 +"~~~~~ fun make_environments , args:"; val (_, []) = (model_patt, i_model);
    1.13  (*\------------------- step into init_calc -------------------------------------------------//*)
    1.14  val (p,_,f,nxt,_,pt) = return_init_calc;
    1.15  
    1.16 @@ -161,8 +161,8 @@
    1.17  (*//////-------------- step into check -------------------------------------------------\\*)
    1.18  "~~~~~ fun check , args:"; val (ctxt, where_rls, pres, (model_patt, i_model)) =
    1.19    (ctxt, where_rls, where_, (pbt, I_Model.OLD_to_TEST pbl));
    1.20 -      val return_of_max_variant =
    1.21 -           of_max_variant model_patt i_model;
    1.22 +      val return_make_environments =
    1.23 +           make_environments model_patt i_model;
    1.24  (*///// //------------ step into of_max_variant --------------------------------------------\\*)
    1.25  "~~~~~ fun of_max_variant , args:"; val (model_patt, i_model) =
    1.26    (model_patt, i_model);
    1.27 @@ -254,9 +254,9 @@
    1.28  (*||||| ||------------ contine of_max_variant ------------------------------------------------*)
    1.29      val subst_eval_list = make_envs_preconds equal_givens
    1.30      val (env_subst, env_eval) = split_list subst_eval_list
    1.31 -val return_of_max_variant = (i_model_max, env_model, (env_subst, env_eval)); (*GOON*)
    1.32 +val make_environments = (i_model_max, env_model, (env_subst, env_eval)); (*GOON*)
    1.33  (*\\\\\ \\------------ step into of_max_variant --------------------------------------------//*)
    1.34 -      val (i_model_max, env_model, (env_subst, env_eval)) = return_of_max_variant
    1.35 +      val (i_model_max, env_model, (env_subst, env_eval)) = make_environments
    1.36  (*!!!/----- we had a helpful argument for constructing env_model and (env_subst, env_eval)---\*)
    1.37        val (i_max_variant, env_model, (env_subst, env_eval)) = (i_model_max, [], ([], []))
    1.38  (*!!!\----- we had a helpful argument for constructing env_model and (env_subst, env_eval)---/*) 
    1.39 @@ -549,7 +549,7 @@
    1.40  "~~~~~ fun check , args:"; val (ctxt, where_rls, pres, (model_patt, i_model)) =
    1.41    (ctxt, where_rls, where_, (pbt, I_Model.OLD_to_TEST pbl));
    1.42  
    1.43 -      val (_, _, (env_subst, env_eval)) = of_max_variant model_patt i_model;
    1.44 +      val (_, (env_subst, env_eval)) = Pre_Conds.make_environments model_patt i_model;
    1.45  "~~~~~ fun of_max_variant , args:"; val (model_patt, i_model) = (model_patt, i_model);
    1.46      val all_variants =
    1.47          map (fn (_, variants, _, _, _) => variants) i_model
    1.48 @@ -648,8 +648,8 @@
    1.49  (*+*)val "[\n(1, [1, 2, 3], true ,#Given, (Cor_TEST Constants [r = 7] , pen2str, Position.T)), \n(2, [1, 2, 3], true ,#Find, (Cor_TEST Maximum A , pen2str, Position.T)), \n(3, [1, 2, 3], true ,#Find, (Cor_TEST AdditionalValues [u, v] , pen2str, Position.T)), \n(4, [1, 2, 3], true ,#Relate, (Cor_TEST Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n(5, [1, 2], true ,#Relate, (Cor_TEST SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T))]"
    1.50   = i_model |> I_Model.to_string_TEST @{context}
    1.51  
    1.52 -val return_of_max_variant as (_, _, (env_subst, env_eval)) =
    1.53 -           of_max_variant model_patt i_model
    1.54 +val return_make_environments as (_, (env_subst, env_eval)) =
    1.55 +           Pre_Conds.make_environments model_patt i_model
    1.56  
    1.57  (*+*)val [(Free ("fixes", T1), Free ("r", T2))] = env_subst (*?!? Const*)
    1.58  (*+*)val Type ("Real.real", []) = T1
    1.59 @@ -658,7 +658,7 @@
    1.60  (*+*)val [(Free ("r", T2), Const ("Num.numeral_class.numeral", _) $ _)] = env_eval
    1.61  (*+*)val Type ("Real.real", []) = T2
    1.62  
    1.63 -val (_, _, (env_subst, env_eval)) = return_of_max_variant;
    1.64 +val (_, (env_subst, env_eval)) = return_make_environments;
    1.65  (*|||----------------- contine check -----------------------------------------------------*)
    1.66        val pres_subst = map (TermC.subst_atomic_all env_subst) pres;
    1.67