1.1 --- a/src/Tools/isac/Interpret/li-tool.sml	Sun Aug 27 16:09:04 2023 +0200
     1.2 +++ b/src/Tools/isac/Interpret/li-tool.sml	Sun Aug 27 16:48:03 2023 +0200
     1.3 @@ -328,7 +328,7 @@
     1.4      val (_, env_model, (env_subst, env_eval)) = I_Model.of_max_variant model_patt i_model;
     1.5      val actuals = map snd env_model
     1.6      val formals = Program.formal_args prog    
     1.7 -    val preconds = Pre_Conds.check_envs_TEST ctxt where_rls where_ (env_model, (env_subst, env_eval))
     1.8 +    val preconds = Pre_Conds.check_envs ctxt where_rls where_ (env_model, (env_subst, env_eval))
     1.9  (*T_TESTnew*)
    1.10      val ctxt = ctxt |> ContextC.insert_assumptions (map snd (snd preconds));
    1.11      val ist = Istate.e_pstate

     2.1 --- a/src/Tools/isac/Interpret/solve-step.sml	Sun Aug 27 16:09:04 2023 +0200
     2.2 +++ b/src/Tools/isac/Interpret/solve-step.sml	Sun Aug 27 16:48:03 2023 +0200
     2.3 @@ -124,7 +124,7 @@
     2.4  (*T_TESTold* )
     2.5          val pres = map (Pre_Conds.environment probl |> subst_atomic) where_
     2.6  ( *T_TEST*)
     2.7 -        val checked = Pre_Conds.check_OLD ctxt where_rls where_ (model, I_Model.OLD_to_TEST probl)
     2.8 +        val checked = Pre_Conds.check ctxt where_rls where_ (model, I_Model.OLD_to_TEST probl)
     2.9          val true_only = checked 
    2.10            |> snd
    2.11            |> map (fn (true, prec) => [prec] | (false, _) => [])

     3.1 --- a/src/Tools/isac/MathEngine/me-misc.sml	Sun Aug 27 16:09:04 2023 +0200
     3.2 +++ b/src/Tools/isac/MathEngine/me-misc.sml	Sun Aug 27 16:48:03 2023 +0200
     3.3 @@ -43,7 +43,7 @@
     3.4  	      else
     3.5  	        let
     3.6  	          val {where_rls, where_, model, ...} = MethodC.from_store ctxt metID
     3.7 -	          val (_, where_) = Pre_Conds.check_OLD ctxt where_rls where_
     3.8 +	          val (_, where_) = Pre_Conds.check ctxt where_rls where_
     3.9                (model, I_Model.OLD_to_TEST meth)
    3.10  		      in where_ end
    3.11  	    val allcorrect = I_Model.is_complete meth andalso foldl and_ (true, (map #1 where_))
    3.12 @@ -73,7 +73,7 @@
    3.13  	      else
    3.14  	        let
    3.15  	          val {where_rls, where_, model, ...} = Problem.from_store ctxt pI
    3.16 -	          val (_, where_) = Pre_Conds.check_OLD ctxt where_rls where_
    3.17 +	          val (_, where_) = Pre_Conds.check ctxt where_rls where_
    3.18                (model, I_Model.OLD_to_TEST probl)
    3.19  	        in where_ end
    3.20  	    val allcorrect = I_Model.is_complete probl andalso foldl and_ (true, (map #1 where_))

     4.1 --- a/src/Tools/isac/Specify/cas-command.sml	Sun Aug 27 16:09:04 2023 +0200
     4.2 +++ b/src/Tools/isac/Specify/cas-command.sml	Sun Aug 27 16:48:03 2023 +0200
     4.3 @@ -84,7 +84,7 @@
     4.4  	  val its_ = map (dtss2itm_ model) dtss (*([1],true,"#Given",Cor (...))*)
     4.5  	  val its = O_Model.add_enumerate its_
     4.6  	  val mits = map flattup2 its
     4.7 -	  val (_, where_) = Pre_Conds.check_OLD ctxt where_rls where_ (model, I_Model.OLD_to_TEST mits)
     4.8 +	  val (_, where_) = Pre_Conds.check ctxt where_rls where_ (model, I_Model.OLD_to_TEST mits)
     4.9      val ctxt = Proof_Context.init_global thy
    4.10    in (pI, pits, mI, mits, where_, ctxt) end;
    4.11  (*T_TESTnew*)

     5.1 --- a/src/Tools/isac/Specify/i-model.sml	Sun Aug 27 16:09:04 2023 +0200
     5.2 +++ b/src/Tools/isac/Specify/i-model.sml	Sun Aug 27 16:48:03 2023 +0200
     5.3 @@ -26,8 +26,6 @@
     5.4    type env
     5.5    type message
     5.6  
     5.7 -  val feedback_to_string: Proof.context -> feedback -> string
     5.8 -  val feedback_TEST_to_string: Proof.context -> feedback_TEST -> string
     5.9    val single_to_string: Proof.context -> single -> string
    5.10    val single_to_string_TEST: Proof.context -> single_TEST -> string
    5.11    val to_string: Proof.context -> T -> string
    5.12 @@ -46,7 +44,7 @@
    5.13    val descriptor_TEST: feedback_TEST -> descriptor
    5.14    val descr_pairs_to_string: Proof.context -> (Model_Pattern.single * single_TEST) list -> string
    5.15    val o_model_values: feedback -> O_Model.values
    5.16 -  val variables_TEST: Model_Pattern.T -> Model_Def.i_model_TEST -> term list
    5.17 +  val variables: Model_Pattern.T -> Model_Def.i_model_TEST -> term list
    5.18    val is_notyet_input : Proof.context -> T -> O_Model.values -> O_Model.single -> Model_Pattern.T
    5.19      -> message * single
    5.20    val get_field_term: theory -> O_Model.single -> single -> m_field * TermC.as_string
    5.21 @@ -66,6 +64,9 @@
    5.22    val eq1: ''a -> 'b * (''a * 'c) -> bool
    5.23  
    5.24  (*from isac_test for Minisubpbl*)
    5.25 +  val feedback_to_string: Proof.context -> feedback -> string
    5.26 +  val feedback_TEST_to_string: Proof.context -> feedback_TEST -> string
    5.27 +
    5.28    val ori_2itm: feedback -> term -> term list -> 'a * 'b * string * descriptor * term list -> 
    5.29      'a * 'b * bool * string * feedback
    5.30    val seek_ppc: int -> T -> single option
    5.31 @@ -230,7 +231,7 @@
    5.32      |> pair2str) equal_descr_pairs)
    5.33    |> strs2str'
    5.34  
    5.35 -fun variables_TEST model_patt i_model =
    5.36 +fun variables model_patt i_model =
    5.37    Pre_Conds.environment_TEST model_patt i_model
    5.38    |> map snd
    5.39  

     6.1 --- a/src/Tools/isac/Specify/m-match.sml	Sun Aug 27 16:09:04 2023 +0200
     6.2 +++ b/src/Tools/isac/Specify/m-match.sml	Sun Aug 27 16:48:03 2023 +0200
     6.3 @@ -97,9 +97,9 @@
     6.4  fun match_oris ctxt where_rls o_model (model_pattern, where_) = 
     6.5    let
     6.6      val i_model = (flat o (map (chk1_ model_pattern))) o_model;
     6.7 -    val mvat = I_Model.variables_TEST model_pattern (I_Model.OLD_to_TEST i_model)
     6.8 +    val mvat = I_Model.variables model_pattern (I_Model.OLD_to_TEST i_model)
     6.9      val complete = chk1_mis mvat i_model model_pattern;
    6.10 -    val (pb, _(*where_'*)) = Pre_Conds.check_OLD ctxt where_rls where_
    6.11 +    val (pb, _(*where_'*)) = Pre_Conds.check ctxt where_rls where_
    6.12        (model_pattern, I_Model.OLD_to_TEST i_model);
    6.13    in if complete andalso pb then true else false end;
    6.14  (*T_TESTnew*)
    6.15 @@ -121,7 +121,7 @@
    6.16      val i_model = (flat o (map (chk1_ model))) o_model;
    6.17      val sups = ((map ori2itmSup) o (filter (field_eq "#undef"))) o_model;
    6.18      val miss = chk1_mis' o_model model;
    6.19 -    val (pb, where_')  = Pre_Conds.check_OLD (Proof_Context.init_global thy) where_rls where_ 
    6.20 +    val (pb, where_')  = Pre_Conds.check (Proof_Context.init_global thy) where_rls where_ 
    6.21        (model, I_Model.OLD_to_TEST i_model);
    6.22    in (miss = [] andalso pb, (i_model @ miss @ sups, where_')) end;
    6.23  (*T_TESTnew*)
    6.24 @@ -174,7 +174,7 @@
    6.25   (*3*)fun mem_vat (_, vats, _, _, _) = member op = vats mv;
    6.26        val newitms = filter mem_vat news;
    6.27   (*4*)val itms' = pbl @ newitms;
    6.28 -      val (pb, where_') = Pre_Conds.check_OLD ctxt where_rls where_ 
    6.29 +      val (pb, where_') = Pre_Conds.check ctxt where_rls where_ 
    6.30          (pbt, I_Model.OLD_to_TEST itms');
    6.31    in (length mis = 0 andalso pb, (itms', where_')) end;
    6.32  (*T_TESTnew*)

     7.1 --- a/src/Tools/isac/Specify/p-spec.sml	Sun Aug 27 16:09:04 2023 +0200
     7.2 +++ b/src/Tools/isac/Specify/p-spec.sml	Sun Aug 27 16:48:03 2023 +0200
     7.3 @@ -205,7 +205,7 @@
     7.4  ( *T_TEST**)
     7.5  	              val {where_rls, where_, model, ...} = Problem.from_store ctxt
     7.6  	                (#2 (References.select_input ospec spec))
     7.7 -		            val (_, where_) = Pre_Conds.check_OLD ctxt where_rls where_
     7.8 +		            val (_, where_) = Pre_Conds.check ctxt where_rls where_
     7.9  		              (model, I_Model.OLD_to_TEST pits)
    7.10  (*T_TESTnew*)
    7.11  	            in (Ctree.update_pbl pt p pits,
    7.12 @@ -220,7 +220,7 @@
    7.13  ( *T_TEST**)
    7.14  	              val {where_rls,where_, model, ...} = MethodC.from_store ctxt 
    7.15  	                (#3 (References.select_input ospec spec))
    7.16 -		            val (_, where_) = Pre_Conds.check_OLD ctxt where_rls where_
    7.17 +		            val (_, where_) = Pre_Conds.check ctxt where_rls where_
    7.18  		              (model, I_Model.OLD_to_TEST mits)
    7.19  (*T_TESTnew*)
    7.20  	            in (Ctree.update_met pt p mits,

     8.1 --- a/src/Tools/isac/Specify/pre-conditions.sml	Sun Aug 27 16:09:04 2023 +0200
     8.2 +++ b/src/Tools/isac/Specify/pre-conditions.sml	Sun Aug 27 16:48:03 2023 +0200
     8.3 @@ -7,11 +7,9 @@
     8.4  sig
     8.5    type T
     8.6    type unchecked
     8.7 -(*RENA unchecked_pos*)
     8.8 -  type unchecked_TEST
     8.9 +  type unchecked_pos
    8.10    type checked
    8.11 -(*RENA checked_pos*)
    8.12 -  type checked_TEST
    8.13 +  type checked_pos
    8.14  
    8.15    type env_subst
    8.16    type env_eval
    8.17 @@ -26,11 +24,11 @@
    8.18    val of_max_variant: Model_Pattern.T -> Model_Def.i_model_TEST ->
    8.19         Model_Def.i_model_TEST * Env.T * (env_subst * env_eval)
    8.20  
    8.21 -  val check_pos: Proof.context -> Rule_Set.T -> unchecked_TEST -> 
    8.22 -    Model_Pattern.T * Model_Def.i_model_TEST -> checked_TEST
    8.23 -  val check_envs_TEST: Proof.context -> Rule_Set.T -> unchecked -> Env.T * (env_subst * env_eval)
    8.24 +  val check_pos: Proof.context -> Rule_Set.T -> unchecked_pos -> 
    8.25 +    Model_Pattern.T * Model_Def.i_model_TEST -> checked_pos
    8.26 +  val check_envs: Proof.context -> Rule_Set.T -> unchecked -> Env.T * (env_subst * env_eval)
    8.27      -> checked
    8.28 -  val check_OLD: Proof.context -> Rule_Set.T -> unchecked ->
    8.29 +  val check: Proof.context -> Rule_Set.T -> unchecked ->
    8.30      Model_Pattern.T * Model_Def.i_model_TEST -> checked
    8.31  
    8.32  (*from isac_test for Minisubpbl*)
    8.33 @@ -38,13 +36,13 @@
    8.34      (Model_Pattern.single * Model_Def.i_model_single_TEST) list
    8.35    val unchecked_OLD_to_TEST: term list -> (term * Position.T) list
    8.36  
    8.37 -  val arrange_args1: int list -> int * Model_Def.variant list -> (int * Model_Def.variant) list
    8.38 +  val arrange_args: int list -> int * Model_Def.variant list -> (int * Model_Def.variant) list
    8.39    val cnt_corrects: Model_Def.i_model_TEST -> int
    8.40  
    8.41    val all_lhs_atoms: term list -> bool
    8.42    val handle_lists: term -> Model_Def.descriptor * term list -> Env.T;
    8.43    val filter_variants': Model_Def.i_model_TEST -> Model_Def.variant -> Model_Def.i_model_TEST
    8.44 -  val switch_type_TEST: Model_Def.descriptor -> term list -> Model_Def.descriptor;
    8.45 +  val switch_type: Model_Def.descriptor -> term list -> Model_Def.descriptor;
    8.46    val discern_feedback: term -> Model_Def.i_model_feedback_TEST ->
    8.47      ((term * term) * (term * term)) list
    8.48    val discern_typ: term -> Model_Pattern.descriptor * term list ->
    8.49 @@ -68,9 +66,9 @@
    8.50  
    8.51  type T = Pre_Conds_Def.T;  (*= (bool * term) list;*)
    8.52  type unchecked = term list
    8.53 -type unchecked_TEST = (term * Position.T) list
    8.54 +type unchecked_pos = (term * Position.T) list
    8.55  type checked = bool * (bool * term) list
    8.56 -type checked_TEST = bool * ((bool * (term * Position.T)) list)
    8.57 +type checked_pos = bool * ((bool * (term * Position.T)) list)
    8.58  
    8.59  (* 
    8.60    we have three kinds of Env.T in the specification-phase:
    8.61 @@ -187,10 +185,10 @@
    8.62          => (mk_env_model id feedb)) equal_descr_pairs
    8.63    |> flat
    8.64  
    8.65 -fun switch_type_TEST descr [] = descr
    8.66 -  | switch_type_TEST (Free (id_string, _)) ts =
    8.67 +fun switch_type descr [] = descr
    8.68 +  | switch_type (Free (id_string, _)) ts =
    8.69      Free (id_string, ts |> hd |> TermC.lhs |> type_of)
    8.70 -  | switch_type_TEST descr _ = raise ERROR ("switch_type_TEST undefined argument " ^
    8.71 +  | switch_type descr _ = raise ERROR ("switch_type undefined argument " ^
    8.72        quote (UnparseC.term (ContextC.for_ERROR ()) descr))
    8.73  
    8.74  fun discern_typ _ (_, []) = []
    8.75 @@ -209,7 +207,7 @@
    8.76      if length ts > 1
    8.77      then (writeln "model items of type 'bool' in lists with 'lengt ts > 1' NOT YET IMPLEMENTED";
    8.78        [])
    8.79 -    else [((switch_type_TEST id ts, TermC.lhs (hd ts)), 
    8.80 +    else [((switch_type id ts, TermC.lhs (hd ts)), 
    8.81             (TermC.lhs (hd ts), TermC.rhs (hd ts)))]
    8.82    else []
    8.83  (*TODO.md "review (descriptor, ts)" REMOVE--------------------------------------\*)
    8.84 @@ -228,9 +226,9 @@
    8.85  (*  filter_variants': Model_Def.i_model_TEST -> Model_Def.variant -> Model_Def.i_model_TEST*)
    8.86  fun filter_variants' i_singles n = 
    8.87    filter (fn (_, variants, _, _, _) => member op= variants n) i_singles
    8.88 -(*arrange_args1: int list -> int * Model_Def.variant list -> (int * Model_Def.variant) list*)
    8.89 -fun arrange_args1 [] _ = []
    8.90 -  | arrange_args1 (sum :: ss) (cnt, all) = (sum, nth cnt all) :: (arrange_args1 ss (cnt + 1, all)) 
    8.91 +(*arrange_args: int list -> int * Model_Def.variant list -> (int * Model_Def.variant) list*)
    8.92 +fun arrange_args [] _ = []
    8.93 +  | arrange_args (sum :: ss) (cnt, all) = (sum, nth cnt all) :: (arrange_args ss (cnt + 1, all)) 
    8.94  (*cnt_corrects: I_Model.T_TEST -> int*)
    8.95  fun cnt_corrects i_model = 
    8.96    fold (curry op +) (map (fn (_, _, _, _, (Cor_TEST _, _)) => 1 | _ => 0) i_model) 0;
    8.97 @@ -244,7 +242,7 @@
    8.98          |> distinct op =
    8.99      val variants_separated = map (filter_variants' i_model) all_variants
   8.100      val sums_corr = map (cnt_corrects) variants_separated
   8.101 -    val sum_variant_s = arrange_args1 sums_corr (1, all_variants)
   8.102 +    val sum_variant_s = arrange_args sums_corr (1, all_variants)
   8.103      val (_, max_variant) = hd (*..crude decision, up to improvement *)
   8.104        (sort (fn ((i, _), (j, _)) => int_ord (i, j)) sum_variant_s)
   8.105      val i_model_max =
   8.106 @@ -278,7 +276,7 @@
   8.107      end;
   8.108  
   8.109  (*takes the envs resulting from of_max_variant*)
   8.110 -fun check_envs_TEST ctxt where_rls where_ (env_model, (env_subst, env_eval)) =
   8.111 +fun check_envs ctxt where_rls where_ (env_model, (env_subst, env_eval)) =
   8.112    let
   8.113        val pres_subst = map (TermC.subst_atomic_all env_subst) where_;
   8.114        val pres_subst_other = map (TermC.subst_atomic_all env_model) (map #2 pres_subst);
   8.115 @@ -290,9 +288,9 @@
   8.116    end
   8.117  
   8.118  (*expects the precondition from Problem, ie. needs substitution by env_model*)
   8.119 -(*TODO: check_OLD shall call check_envs_TEST*)
   8.120 -fun check_OLD _ _ [] _  = (true, [])
   8.121 -  | check_OLD ctxt where_rls where_ (model_patt, i_model) =
   8.122 +(*TODO: check shall call check_envs*)
   8.123 +fun check _ _ [] _  = (true, [])
   8.124 +  | check ctxt where_rls where_ (model_patt, i_model) =
   8.125      let
   8.126        val (_, env_model, (env_subst, env_eval)) = of_max_variant model_patt i_model
   8.127        val pres_subst = map (TermC.subst_atomic_all env_subst) where_;

     9.1 --- a/src/Tools/isac/Specify/refine.sml	Sun Aug 27 16:09:04 2023 +0200
     9.2 +++ b/src/Tools/isac/Specify/refine.sml	Sun Aug 27 16:48:03 2023 +0200
     9.3 @@ -144,7 +144,7 @@
     9.4  	  val itms'' = filter (okv mvat) itms';
     9.5  	  val untouched = filter eq0 itms; (* i.e. dsc only (from init)*)
     9.6  	  val mis = chk_mis mvat itms'' untouched pbt;
     9.7 -	  val (pb, where_')  = Pre_Conds.check_OLD (Proof_Context.init_global thy) where_rls where_
     9.8 +	  val (pb, where_')  = Pre_Conds.check (Proof_Context.init_global thy) where_rls where_
     9.9  	    (pbt, I_Model.OLD_to_TEST itms'')
    9.10    in (length mis = 0 andalso pb, (itms'@ mis, where_')) end;
    9.11  (*T_TESTnew*)

    10.1 --- a/src/Tools/isac/Specify/specification.sml	Sun Aug 27 16:09:04 2023 +0200
    10.2 +++ b/src/Tools/isac/Specify/specification.sml	Sun Aug 27 16:48:03 2023 +0200
    10.3 @@ -124,7 +124,7 @@
    10.4  ( *T_TEST**)
    10.5        val {where_rls, where_, model, ...} =
    10.6          Problem.from_store ctxt (#2 (References.select_input ospec spec))
    10.7 -      val (_, where_) = Pre_Conds.check_OLD ctxt where_rls where_ 
    10.8 +      val (_, where_) = Pre_Conds.check ctxt where_rls where_ 
    10.9          (model, I_Model.OLD_to_TEST probl)
   10.10  (*T_TESTnew*)
   10.11      in
   10.12 @@ -139,7 +139,7 @@
   10.13  ( *T_TEST**)
   10.14        val {where_rls, where_, model, ...} =
   10.15          MethodC.from_store ctxt (#3 (References.select_input ospec spec))
   10.16 -      val (_, where_)  = Pre_Conds.check_OLD ctxt where_rls where_ 
   10.17 +      val (_, where_)  = Pre_Conds.check ctxt where_rls where_ 
   10.18          (model, I_Model.OLD_to_TEST meth)
   10.19  (*T_TESTnew*)
   10.20      in

    11.1 --- a/src/Tools/isac/Specify/specify.sml	Sun Aug 27 16:09:04 2023 +0200
    11.2 +++ b/src/Tools/isac/Specify/specify.sml	Sun Aug 27 16:48:03 2023 +0200
    11.3 @@ -82,7 +82,7 @@
    11.4      val cmI = if mI = MethodC.id_empty then mI' else mI;
    11.5      val {model = pbt, where_rls, where_, ...} = Problem.from_store ctxt cpI;
    11.6      val {model = mpc, ...} = MethodC.from_store ctxt cmI
    11.7 -    val (preok, _) = Pre_Conds.check_OLD ctxt where_rls where_ (pbt, I_Model.OLD_to_TEST pbl);
    11.8 +    val (preok, _) = Pre_Conds.check ctxt where_rls where_ (pbt, I_Model.OLD_to_TEST pbl);
    11.9    in
   11.10      if dI' = ThyC.id_empty andalso dI = ThyC.id_empty then
   11.11        ("dummy", (Pos.Pbl, Tactic.Specify_Theory dI'))
   11.12 @@ -118,7 +118,7 @@
   11.13    let
   11.14      val cmI = if mI = MethodC.id_empty then mI' else mI;
   11.15      val {model = mpc, where_rls, where_, ...} = MethodC.from_store ctxt cmI;
   11.16 -    val (preok, _) = Pre_Conds.check_OLD ctxt where_rls where_ (mpc, I_Model.OLD_to_TEST met);
   11.17 +    val (preok, _) = Pre_Conds.check ctxt where_rls where_ (mpc, I_Model.OLD_to_TEST met);
   11.18    in
   11.19      (case find_first (I_Model.is_error o #5) met of
   11.20        SOME (_,_,_, fd, itm_) =>

    12.1 --- a/test/Tools/isac/BridgeJEdit/template.sml	Sun Aug 27 16:09:04 2023 +0200
    12.2 +++ b/test/Tools/isac/BridgeJEdit/template.sml	Sun Aug 27 16:48:03 2023 +0200
    12.3 @@ -62,7 +62,7 @@
    12.4  (*+*)then () else error "final test of build I_Model.init_TEST FAILED";
    12.5  
    12.6        val {where_rls, where_, ...} = MethodC.from_store ctxt meth_id;
    12.7 -      val (_, preconds) = Pre_Conds.check_OLD ctxt where_rls where_ (model_patt, empty_i_model);
    12.8 +      val (_, preconds) = Pre_Conds.check ctxt where_rls where_ (model_patt, empty_i_model);
    12.9  
   12.10             show ctxt preconds empty_i_model in_refs;
   12.11  "~~~~~ fun show , args:"; val (ctxt, preconds, i_model, in_refs) =

    13.1 --- a/test/Tools/isac/Interpret/li-tool.sml	Sun Aug 27 16:09:04 2023 +0200
    13.2 +++ b/test/Tools/isac/Interpret/li-tool.sml	Sun Aug 27 16:48:03 2023 +0200
    13.3 @@ -368,7 +368,7 @@
    13.4          |> distinct op =
    13.5      val variants_separated = map (filter_variants' i_model) all_variants
    13.6      val sums_corr = map (cnt_corrects) variants_separated
    13.7 -    val sum_variant_s = arrange_args1 sums_corr (1, all_variants)
    13.8 +    val sum_variant_s = arrange_args sums_corr (1, all_variants)
    13.9      val (_, max_variant) = hd (*..crude decision, up to improvement *)
   13.10        (sort (fn ((i, _), (j, _)) => int_ord (i, j)) sum_variant_s)
   13.11      val i_model_max =
   13.12 @@ -443,7 +443,7 @@
   13.13  (*+*)val 9 = length formals
   13.14  
   13.15      val preconds =
   13.16 -      Pre_Conds.check_envs_TEST ctxt where_rls where_ (env_model, (env_subst, env_eval))
   13.17 +      Pre_Conds.check_envs ctxt where_rls where_ (env_model, (env_subst, env_eval))
   13.18      val ctxt = ctxt |> ContextC.insert_assumptions (map snd (snd preconds));
   13.19      val ist = Istate.e_pstate
   13.20        |> Istate.set_eval prog_rls

    14.1 --- a/test/Tools/isac/Knowledge/eqsystem-1.sml	Sun Aug 27 16:09:04 2023 +0200
    14.2 +++ b/test/Tools/isac/Knowledge/eqsystem-1.sml	Sun Aug 27 16:48:03 2023 +0200
    14.3 @@ -596,8 +596,8 @@
    14.4      val {model = mpc, ...} = MethodC.from_store ctxt cmI
    14.5  
    14.6  (** )val (preok, _) =
    14.7 - Pre_Conds.check_OLD ctxt where_rls where_ (pbt, I_Model.OLD_to_TEST pbl); ( **);
    14.8 -"~~~~~ fun check_OLD , args:"; val (ctxt, where_rls, pres, (model_patt, i_model)) =
    14.9 + Pre_Conds.check ctxt where_rls where_ (pbt, I_Model.OLD_to_TEST pbl); ( **);
   14.10 +"~~~~~ fun check , args:"; val (ctxt, where_rls, pres, (model_patt, i_model)) =
   14.11    (ctxt, where_rls, where_, (pbt, I_Model.OLD_to_TEST pbl));
   14.12  
   14.13  (*WN230827: REPLACE WITH I_Model.of_max_variant* )val (env_subst, env_eval) =

    15.1 --- a/test/Tools/isac/Knowledge/simplify.sml	Sun Aug 27 16:09:04 2023 +0200
    15.2 +++ b/test/Tools/isac/Knowledge/simplify.sml	Sun Aug 27 16:48:03 2023 +0200
    15.3 @@ -112,7 +112,7 @@
    15.4      val cmI = if mI = MethodC.id_empty then mI' else mI;
    15.5      val {model = mpc, where_rls, where_, ...} = MethodC.from_store ctxt cmI;
    15.6  
    15.7 -(**) val (preok as true, _) = Pre_Conds.check_OLD ctxt where_rls where_ (mpc, I_Model.OLD_to_TEST met);
    15.8 +(**) val (preok as true, _) = Pre_Conds.check ctxt where_rls where_ (mpc, I_Model.OLD_to_TEST met);
    15.9  (*\------------------- step into autoCalculate 1 (Steps 1) \<longrightarrow> Apply_Method ----------------/*)
   15.10  val ((pt,p),_) = States.get_calc 1;  
   15.11  Test_Tool.show_pt pt;

    16.1 --- a/test/Tools/isac/Minisubpbl/100-init-rootpbl-NEXT_STEP.sml	Sun Aug 27 16:09:04 2023 +0200
    16.2 +++ b/test/Tools/isac/Minisubpbl/100-init-rootpbl-NEXT_STEP.sml	Sun Aug 27 16:48:03 2023 +0200
    16.3 @@ -57,11 +57,11 @@
    16.4      val {model = pbt, where_rls, where_, ...} = Problem.from_store ctxt cpI;
    16.5      val {model = mpc, ...} = MethodC.from_store ctxt cmI
    16.6      val (preok as true, xxx) =
    16.7 - Pre_Conds.check_OLD ctxt where_rls where_ (pbt, I_Model.OLD_to_TEST pbl);
    16.8 + Pre_Conds.check ctxt where_rls where_ (pbt, I_Model.OLD_to_TEST pbl);
    16.9  (*+*)val "[\n(1, [1], true ,#Given, (Cor_TEST equality (x + 1 = 2) ,(e_e, [x + 1 = 2]), Position.T)), \n(2, [1], true ,#Given, (Cor_TEST solveFor x ,(v_v, [x]), Position.T)), \n(3, [1], true ,#Find, (Cor_TEST solutions L ,(v_v'i', [L]), Position.T))]"
   16.10    = I_Model.OLD_to_TEST pbl |> I_Model.to_string_TEST @{context};
   16.11  (*+*)val "[precond_rootpbl v_v]" = where_ |> UnparseC.terms @{context};
   16.12 -"~~~~~ fun check_OLD , args:"; val (ctxt, where_rls, pres, (model_patt, i_model)) =
   16.13 +"~~~~~ fun check , args:"; val (ctxt, where_rls, pres, (model_patt, i_model)) =
   16.14    (ctxt, where_rls, where_, (pbt, I_Model.OLD_to_TEST pbl));
   16.15        val (_, env_model, (env_subst, env_eval)) = of_max_variant model_patt i_model
   16.16        val pres_subst = map (TermC.subst_atomic_all env_subst) pres;
   16.17 @@ -137,8 +137,8 @@
   16.18   (*4*)val itms' = pbl @ newitms;
   16.19  
   16.20        val (pb, where_') =
   16.21 - Pre_Conds.check_OLD ctxt where_rls where_ (m_patt, I_Model.OLD_to_TEST itms');
   16.22 -"~~~~~ fun check_OLD , args:"; val (ctxt, where_rls, pres, (model_patt, i_model)) =
   16.23 + Pre_Conds.check ctxt where_rls where_ (m_patt, I_Model.OLD_to_TEST itms');
   16.24 +"~~~~~ fun check , args:"; val (ctxt, where_rls, pres, (model_patt, i_model)) =
   16.25    (ctxt, where_rls, where_, (m_patt, I_Model.OLD_to_TEST itms'));
   16.26        val (_, env_model, (env_subst, env_eval)) = of_max_variant model_patt i_model
   16.27        val pres_subst = map (TermC.subst_atomic_all env_subst) pres;
   16.28 @@ -298,7 +298,7 @@
   16.29      val sums_corr = map (cnt_corrects) variants_separated
   16.30  (*+*)val [3] = sums_corr;
   16.31  
   16.32 -    val sum_variant_s = arrange_args1 sums_corr (1, all_variants)
   16.33 +    val sum_variant_s = arrange_args sums_corr (1, all_variants)
   16.34  (*+*)val [(3, 1)] = sum_variant_s;
   16.35  
   16.36      val (_, max_variant) = hd (*..crude decision, up to improvement *)
   16.37 @@ -350,7 +350,7 @@
   16.38  (*+*)val "minisubpbl e_e v_v =\n(let e_ea =\n       (Try (Rewrite_Set ''norm_equation'') #>\n        Try (Rewrite_Set ''Test_simplify''))\n        e_e;\n     L_La =\n       SubProblem\n        (''Test'', [''LINEAR'', ''univariate'', ''equation'', ''test''],\n         [''Test'', ''solve_linear''])\n        [BOOL e_e, REAL v_v]\n in Check_elementwise L_L {v_v. Assumptions})" =
   16.39    (prog |> UnparseC.term @{context})
   16.40  
   16.41 -    val preconds = Pre_Conds.check_envs_TEST ctxt where_rls where_ (env_model, (env_subst, env_eval))
   16.42 +    val preconds = Pre_Conds.check_envs ctxt where_rls where_ (env_model, (env_subst, env_eval))
   16.43  
   16.44  (*||------------------ continue init_pstate ------------------------------------------------\\*)
   16.45      val ctxt = ctxt |> ContextC.insert_assumptions (map snd (snd preconds));

    17.1 --- a/test/Tools/isac/Minisubpbl/150a-add-given-Maximum.sml	Sun Aug 27 16:09:04 2023 +0200
    17.2 +++ b/test/Tools/isac/Minisubpbl/150a-add-given-Maximum.sml	Sun Aug 27 16:48:03 2023 +0200
    17.3 @@ -70,9 +70,9 @@
    17.4                 (*if*) pI = Problem.id_empty (*else*);
    17.5  	          val {where_rls, where_, model, ...} = Problem.from_store ctxt pI
    17.6  	          val (_, where_) = 
    17.7 - Pre_Conds.check_OLD ctxt where_rls where_
    17.8 + Pre_Conds.check ctxt where_rls where_
    17.9                (model, I_Model.OLD_to_TEST probl);
   17.10 -"~~~~~ fun check_OLD , args:"; val (ctxt, where_rls, pres, (model_patt, i_model)) =
   17.11 +"~~~~~ fun check , args:"; val (ctxt, where_rls, pres, (model_patt, i_model)) =
   17.12    (ctxt, where_rls, where_, (model, I_Model.OLD_to_TEST probl));
   17.13        val (_, _, (env_subst, env_eval)) =
   17.14             of_max_variant model_patt i_model;
   17.15 @@ -156,12 +156,12 @@
   17.16      val {model = pbt, where_rls, where_, ...} = Problem.from_store ctxt cpI;
   17.17      val {model = mpc, ...} = MethodC.from_store ctxt cmI;
   17.18  (*//------------------ adhoc inserted fun of_max_variant -----------------------------------\\*)
   17.19 -(*\\------------------ adhoc inserted fun check_OLD ----------------------------------------//*)
   17.20 +(*\\------------------ adhoc inserted fun check ----------------------------------------//*)
   17.21  
   17.22      val return_check_OLD =
   17.23 -           check_OLD ctxt where_rls where_ (pbt, I_Model.OLD_to_TEST pbl);
   17.24 -(*//////-------------- step into check_OLD -------------------------------------------------\\*)
   17.25 -"~~~~~ fun check_OLD , args:"; val (ctxt, where_rls, pres, (model_patt, i_model)) =
   17.26 +           check ctxt where_rls where_ (pbt, I_Model.OLD_to_TEST pbl);
   17.27 +(*//////-------------- step into check -------------------------------------------------\\*)
   17.28 +"~~~~~ fun check , args:"; val (ctxt, where_rls, pres, (model_patt, i_model)) =
   17.29    (ctxt, where_rls, where_, (pbt, I_Model.OLD_to_TEST pbl));
   17.30        val return_of_max_variant =
   17.31             of_max_variant model_patt i_model;
   17.32 @@ -181,7 +181,7 @@
   17.33          |> distinct op =
   17.34      val variants_separated = map (filter_variants' i_model) all_variants
   17.35      val sums_corr = map (cnt_corrects) variants_separated
   17.36 -    val sum_variant_s = arrange_args1 sums_corr (1, all_variants)
   17.37 +    val sum_variant_s = arrange_args sums_corr (1, all_variants)
   17.38  (*+*)val [(0, 1), (0, 2), (0, 3)] = sum_variant_s
   17.39      val (_, max_variant) = hd (*..crude decision, up to improvement *)
   17.40        (sort (fn ((i, _), (j, _)) => int_ord (i, j)) sum_variant_s)
   17.41 @@ -246,8 +246,8 @@
   17.42  ( *nth 2 equal_descr_pairs*)
   17.43  (*+*)val [] = return_discern_typ;
   17.44  (**)
   17.45 -           switch_type_TEST id ts;
   17.46 -"~~~~~ fun switch_type_TEST , args:"; val (Const (descr_string, _), ts) = (descr, ts);
   17.47 +           switch_type id ts;
   17.48 +"~~~~~ fun switch_type , args:"; val (Const (descr_string, _), ts) = (descr, ts);
   17.49  
   17.50  (*nth 1 equal_descr_pairs* )
   17.51  val return_switch_type_TEST = Const (descr_string, ts |> hd |> TermC.lhs |> type_of)
   17.52 @@ -267,14 +267,14 @@
   17.53  (*!!!/----- we had a helpful argument for constructing env_model and (env_subst, env_eval)---\*)
   17.54        val (i_max_variant, env_model, (env_subst, env_eval)) = (i_model_max, [], ([], []))
   17.55  (*!!!\----- we had a helpful argument for constructing env_model and (env_subst, env_eval)---/*) 
   17.56 -(*||||||-------------- contine check_OLD -----------------------------------------------------*)
   17.57 +(*||||||-------------- contine check -----------------------------------------------------*)
   17.58        val pres_subst = map (TermC.subst_atomic_all env_subst) pres;
   17.59        val pres_subst_other = map (TermC.subst_atomic_all env_model) (map #2 pres_subst);
   17.60        val full_subst = if env_eval = [] then pres_subst_other
   17.61          else map (TermC.subst_atomic_all env_eval) (map #2 pres_subst_other)
   17.62        val evals = map (eval ctxt where_rls) full_subst
   17.63  val return_ = (i_model_max, env_subst, env_eval)
   17.64 -(*\\\\\\\------------- step into check_OLD -------------------------------------------------//*)
   17.65 +(*\\\\\\\------------- step into check -------------------------------------------------//*)
   17.66  val (preok, _) = return_check_OLD;
   17.67  
   17.68  (*|||||--------------- contine for_problem ---------------------------------------------------*)
   17.69 @@ -435,7 +435,7 @@
   17.70  (*      else                                       *)
   17.71  (*        let                                      *)
   17.72  	          val {where_rls, where_, model, ...} = Problem.from_store ctxt pI
   17.73 -	          val (_, where_) = (*Pre_Conds.*)check_OLD ctxt where_rls where_ (model, I_Model.OLD_to_TEST probl)
   17.74 +	          val (_, where_) = (*Pre_Conds.*)check ctxt where_rls where_ (model, I_Model.OLD_to_TEST probl)
   17.75  (*        in where_ end                           *)
   17.76  	    val allcorrect = I_Model.is_complete probl andalso foldl and_ (true, (map #1 where_))
   17.77  val return_pt_model = Ctree.ModSpec (allcorrect, Pos.Pbl, hdl, probl, where_, spec)
   17.78 @@ -489,7 +489,7 @@
   17.79  (*//------------------ step into Step.by_tactic --------------------------------------------\\*)
   17.80  "~~~~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, p));
   17.81  val Applicable.Yes tac' =
   17.82 -    (*case*) check tac (pt, p) (*of*);
   17.83 +    (*case*) Specify_Step.check tac (pt, p) (*of*);
   17.84  	    (*if*) Tactic.for_specify' tac' (*then*);
   17.85  Step_Specify.by_tactic tac' ptp;
   17.86  "~~~~~ fun by_tactic , args:"; val ((Tactic.Add_Given' (ct, _)), (pt, p)) = (tac', ptp);
   17.87 @@ -559,8 +559,8 @@
   17.88      val {model = mpc, ...} = MethodC.from_store ctxt cmI
   17.89  
   17.90      val (preok, _) =
   17.91 -Pre_Conds.check_OLD ctxt where_rls where_ (pbt, I_Model.OLD_to_TEST pbl);
   17.92 -"~~~~~ fun check_OLD , args:"; val (ctxt, where_rls, pres, (model_patt, i_model)) =
   17.93 +Pre_Conds.check ctxt where_rls where_ (pbt, I_Model.OLD_to_TEST pbl);
   17.94 +"~~~~~ fun check , args:"; val (ctxt, where_rls, pres, (model_patt, i_model)) =
   17.95    (ctxt, where_rls, where_, (pbt, I_Model.OLD_to_TEST pbl));
   17.96  
   17.97        val (_, _, (env_subst, env_eval)) = of_max_variant model_patt i_model;
   17.98 @@ -571,7 +571,7 @@
   17.99          |> distinct op =
  17.100      val variants_separated = map (filter_variants' i_model) all_variants
  17.101      val sums_corr = map (cnt_corrects) variants_separated
  17.102 -    val sum_variant_s = arrange_args1 sums_corr (1, all_variants)
  17.103 +    val sum_variant_s = arrange_args sums_corr (1, all_variants)
  17.104      val (_, max_variant) = hd (*..crude decision, up to improvement *)
  17.105        (sort (fn ((i, _), (j, _)) => int_ord (i, j)) sum_variant_s)
  17.106      val i_model_max =
  17.107 @@ -652,9 +652,9 @@
  17.108    Free ("fixes", _)] = where_
  17.109  
  17.110      val (preok, _) =
  17.111 - Pre_Conds.check_OLD ctxt where_rls where_ (pbt, I_Model.OLD_to_TEST pbl);
  17.112 -(*///----------------- step into check_OLD -------------------------------------------------\\*)
  17.113 -"~~~~~ fun check_OLD , args:"; val (ctxt, where_rls, pres, (model_patt, i_model)) =
  17.114 + Pre_Conds.check ctxt where_rls where_ (pbt, I_Model.OLD_to_TEST pbl);
  17.115 +(*///----------------- step into check -------------------------------------------------\\*)
  17.116 +"~~~~~ fun check , args:"; val (ctxt, where_rls, pres, (model_patt, i_model)) =
  17.117    (ctxt, where_rls, where_, (pbt, I_Model.OLD_to_TEST pbl));
  17.118  (*+*)val "[0 < fixes]" = pres |> UnparseC.terms @{context}
  17.119  (*+*)val "[\"(#Given, (Constants, fixes))\", \"(#Find, (Maximum, maxx))\", \"(#Find, (AdditionalValues, vals))\", \"(#Relate, (Extremum, extr))\", \"(#Relate, (SideConditions, sideconds))\"]"
  17.120 @@ -673,10 +673,10 @@
  17.121  (*+*)val Type ("Real.real", []) = T2
  17.122  
  17.123  val (_, _, (env_subst, env_eval)) = return_of_max_variant;
  17.124 -(*|||----------------- contine check_OLD -----------------------------------------------------*)
  17.125 +(*|||----------------- contine check -----------------------------------------------------*)
  17.126        val pres_subst = map (TermC.subst_atomic_all env_subst) pres;
  17.127  
  17.128 -(*|||----------------- contine check_OLD -----------------------------------------------------*)
  17.129 +(*|||----------------- contine check -----------------------------------------------------*)
  17.130  (*+*)val [(true, Const ("Orderings.ord_class.less", _) $
  17.131    Const ("Groups.zero_class.zero", _) $ Free ("r", _))] = pres_subst
  17.132  
  17.133 @@ -687,7 +687,7 @@
  17.134  
  17.135        val evals = map (eval ctxt where_rls) full_subst
  17.136  val return_check_OLD = (foldl and_ (true, map fst evals), pres_subst)
  17.137 -(*\\\----------------- step into check_OLD -------------------------------------------------\\*)
  17.138 +(*\\\----------------- step into check -------------------------------------------------\\*)
  17.139  
  17.140      val (preok as true, _) = return_check_OLD
  17.141  (*+---------------^^^^*)
  17.142 @@ -708,7 +708,7 @@
  17.143        Step.by_tactic tac (pt, p);
  17.144  (*//------------------ step into Step_by_tactic --------------------------------------------\\*)
  17.145  "~~~~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, p));
  17.146 -    (*case*) check tac (pt, p) (*of*);
  17.147 +    (*case*) Specify_Step.check tac (pt, p) (*of*);
  17.148  
  17.149  (*||------------------ contine Step_by_tactic ------------------------------------------------*)
  17.150  (*\\------------------ step into Step_by_tactic --------------------------------------------//*)
  17.151 @@ -857,7 +857,7 @@
  17.152    = (ctxt, oris, (o_refs, refs), (pbl, met));
  17.153      val cmI = if mI = MethodC.id_empty then mI' else mI;
  17.154      val {model, where_rls, where_, ...} = MethodC.from_store ctxt cmI;    (*..MethodC ?*)
  17.155 -    val (preok, _) = Pre_Conds.check_OLD ctxt where_rls where_ (model, I_Model.OLD_to_TEST met);
  17.156 +    val (preok, _) = Pre_Conds.check ctxt where_rls where_ (model, I_Model.OLD_to_TEST met);
  17.157  val NONE =
  17.158      (*case*) find_first (I_Model.is_error o #5) met (*of*);
  17.159  

    18.1 --- a/test/Tools/isac/Minisubpbl/200-start-method-NEXT_STEP.sml	Sun Aug 27 16:09:04 2023 +0200
    18.2 +++ b/test/Tools/isac/Minisubpbl/200-start-method-NEXT_STEP.sml	Sun Aug 27 16:48:03 2023 +0200
    18.3 @@ -81,9 +81,9 @@
    18.4        val newitms = filter mem_vat news;
    18.5   (*4*)val itms' = pbl @ newitms;
    18.6  
    18.7 -      val (pb, where_') = Pre_Conds.check_OLD ctxt where_rls where_ 
    18.8 +      val (pb, where_') = Pre_Conds.check ctxt where_rls where_ 
    18.9          (pbt, I_Model.OLD_to_TEST itms');
   18.10 -"~~~~~ fun check_OLD , args:"; val (ctxt, where_rls, where_, (model_patt, i_model)) =
   18.11 +"~~~~~ fun check , args:"; val (ctxt, where_rls, where_, (model_patt, i_model)) =
   18.12    (ctxt, where_rls, where_, (pbt, I_Model.OLD_to_TEST itms'));
   18.13        val (_, env_model, (env_subst, env_eval)) = of_max_variant model_patt i_model
   18.14        val pres_subst = map (TermC.subst_atomic_all env_subst) where_;
   18.15 @@ -239,7 +239,7 @@
   18.16  (*+*)val "minisubpbl e_e v_v =\n(let e_ea =\n       (Try (Rewrite_Set ''norm_equation'') #>\n        Try (Rewrite_Set ''Test_simplify''))\n        e_e;\n     L_La =\n       SubProblem\n        (''Test'', [''LINEAR'', ''univariate'', ''equation'', ''test''],\n         [''Test'', ''solve_linear''])\n        [BOOL e_e, REAL v_v]\n in Check_elementwise L_L {v_v. Assumptions})" =
   18.17    (prog |> UnparseC.term @{context})
   18.18  
   18.19 -    val preconds = Pre_Conds.check_envs_TEST ctxt where_rls where_ (env_model, (env_subst, env_eval))
   18.20 +    val preconds = Pre_Conds.check_envs ctxt where_rls where_ (env_model, (env_subst, env_eval))
   18.21  
   18.22  (*||------------------ continue init_pstate NEW --------------------------------------------\\*)
   18.23      val ctxt = ctxt |> ContextC.insert_assumptions (map snd (snd preconds));

    19.1 --- a/test/Tools/isac/Minisubpbl/400-start-meth-subpbl.sml	Sun Aug 27 16:09:04 2023 +0200
    19.2 +++ b/test/Tools/isac/Minisubpbl/400-start-meth-subpbl.sml	Sun Aug 27 16:48:03 2023 +0200
    19.3 @@ -85,7 +85,7 @@
    19.4      val {model = mpc, ...} = MethodC.from_store ctxt cmI
    19.5  
    19.6  val (preok, xxxxx) =
    19.7 - Pre_Conds.check_OLD ctxt where_rls where_ (pbt, I_Model.OLD_to_TEST pbl);
    19.8 + Pre_Conds.check ctxt where_rls where_ (pbt, I_Model.OLD_to_TEST pbl);
    19.9  
   19.10  (*+*)val [(true, xxx)] = xxxxx;
   19.11  (*+*)if (xxx |> UnparseC.term @{context}) =
   19.12 @@ -95,7 +95,7 @@
   19.13    "matches (?a + ?b * x = 0) (- 1 + x = 0)"
   19.14    then () else error "pre-cond, to be evaluated, CHANGED";
   19.15  
   19.16 -"~~~~~ fun check_OLD , args:"; val (ctxt, where_rls, pres, (model_patt, i_model)) =
   19.17 +"~~~~~ fun check , args:"; val (ctxt, where_rls, pres, (model_patt, i_model)) =
   19.18    (ctxt, where_rls, where_, (pbt, OLD_to_TEST pbl)); (*..delete double above --- adhoc inserted n ---*)
   19.19  
   19.20        val (_, env_model, (env_subst, env_eval)) = 
   19.21 @@ -117,7 +117,7 @@
   19.22          |> distinct op =
   19.23      val variants_separated = map (filter_variants' i_model) all_variants
   19.24      val sums_corr = map (cnt_corrects) variants_separated
   19.25 -    val sum_variant_s = arrange_args1 sums_corr (1, all_variants)
   19.26 +    val sum_variant_s = arrange_args sums_corr (1, all_variants)
   19.27      val (_, max_variant) = hd (*..crude decision, up to improvement *)
   19.28        (sort (fn ((i, _), (j, _)) => int_ord (i, j)) sum_variant_s)
   19.29      val i_model_max =

    20.1 --- a/test/Tools/isac/Specify/pre-conditions.sml	Sun Aug 27 16:09:04 2023 +0200
    20.2 +++ b/test/Tools/isac/Specify/pre-conditions.sml	Sun Aug 27 16:48:03 2023 +0200
    20.3 @@ -111,7 +111,7 @@
    20.4  val return_check_pos =
    20.5        (foldl and_ (true, map (fn ((bool, _: term), _: Position.T) => bool) evals), display)
    20.6  :
    20.7 -checked_TEST
    20.8 +checked_pos
    20.9  
   20.10  (* final test ... ----------------------------------------------------------------------------*)
   20.11  val (true, [(true, (Const ("Orderings.ord_class.less", _) $ 

    21.1 --- a/test/Tools/isac/Specify/refine.sml	Sun Aug 27 16:09:04 2023 +0200
    21.2 +++ b/test/Tools/isac/Specify/refine.sml	Sun Aug 27 16:48:03 2023 +0200
    21.3 @@ -394,12 +394,12 @@
    21.4    = model_pattern |> Model_Pattern.to_string @{context}
    21.5  (*+*)val "[Length e_s = 4, Length v_s = 4]" = where_ |> UnparseC.terms @{context}
    21.6  
    21.7 -   val mvat = I_Model.variables_TEST model_pattern (I_Model.OLD_to_TEST i_model)
    21.8 +   val mvat = I_Model.variables model_pattern (I_Model.OLD_to_TEST i_model)
    21.9      val complete = chk1_mis mvat i_model model_pattern;
   21.10  
   21.11      val (pb as true, (** )_( **)where_'(**)) =
   21.12 - Pre_Conds.check_OLD ctxt where_rls where_ (model_pattern, I_Model.OLD_to_TEST i_model);
   21.13 -"~~~~~ fun check_OLD , args:"; val (ctxt, where_rls, pres, (model_patt, i_model)) =
   21.14 + Pre_Conds.check ctxt where_rls where_ (model_pattern, I_Model.OLD_to_TEST i_model);
   21.15 +"~~~~~ fun check , args:"; val (ctxt, where_rls, pres, (model_patt, i_model)) =
   21.16    (ctxt, where_rls, where_, (model_pattern, I_Model.OLD_to_TEST i_model));
   21.17  
   21.18  (*+*)val [(true, xxx), (true, yyy)] = where_'
   21.19 @@ -415,7 +415,7 @@
   21.20          |> distinct op =
   21.21      val variants_separated = map (filter_variants' i_model) all_variants
   21.22      val sums_corr = map (cnt_corrects) variants_separated
   21.23 -    val sum_variant_s = arrange_args1 sums_corr (1, all_variants)
   21.24 +    val sum_variant_s = arrange_args sums_corr (1, all_variants)
   21.25      val (_, max_variant) = hd (*..crude decision, up to improvement *)
   21.26        (sort (fn ((i, _), (j, _)) => int_ord (i, j)) sum_variant_s)
   21.27      val i_model_max =
   21.28 @@ -451,7 +451,7 @@
   21.29    (*if*)  Model_Pattern.typ_of_element descr = HOLogic.boolT (*then*);
   21.30  
   21.31  (*+*)val false = all_lhs_atoms ts
   21.32 -(*-------------------- contine check_OLD -----------------------------------------------------*)
   21.33 +(*-------------------- contine check -----------------------------------------------------*)
   21.34  
   21.35       val pres_subst = map (TermC.subst_atomic_all env_subst) where_;
   21.36  
   21.37 @@ -573,7 +573,7 @@
   21.38      val cmI = if mI = MethodC.id_empty then mI' else mI;
   21.39      val {model = pbt, where_rls, where_, ...} = Problem.from_store ctxt cpI;
   21.40      val {model = mpc, ...} = MethodC.from_store ctxt cmI
   21.41 -    val (preok, _) = Pre_Conds.check_OLD ctxt where_rls where_ (pbt, I_Model.OLD_to_TEST pbl);
   21.42 +    val (preok, _) = Pre_Conds.check ctxt where_rls where_ (pbt, I_Model.OLD_to_TEST pbl);
   21.43      (*if*) dI' = ThyC.id_empty andalso dI = ThyC.id_empty (*else*);
   21.44        (*if*) pI' = Problem.id_empty andalso pI = Problem.id_empty (*else*);
   21.45        val NONE = (*case*) find_first (I_Model.is_error o #5) pbl (*of*);

    22.1 --- a/test/Tools/isac/Specify/specify.sml	Sun Aug 27 16:09:04 2023 +0200
    22.2 +++ b/test/Tools/isac/Specify/specify.sml	Sun Aug 27 16:48:03 2023 +0200
    22.3 @@ -594,7 +594,7 @@
    22.4    (oris, (o_refs, refs), (pbl, met));
    22.5      val cmI = if mI = MethodC.id_empty then mI' else mI;
    22.6      val {model = mpc, where_rls, where_, ...} = MethodC.from_store ctxt cmI;
    22.7 -    val (preok, _) = Pre_Conds.check_OLD ctxt where_rls where_ (mpc, I_Model.OLD_to_TEST met);
    22.8 +    val (preok, _) = Pre_Conds.check ctxt where_rls where_ (mpc, I_Model.OLD_to_TEST met);
    22.9  "~~~~~ from fun find_next_step \<longrightarrow>fun specify_do_next , return:"; val (_, (p_', tac)) = (return);
   22.10  (*/------------------- check within find_next_step -----------------------------------------\*)
   22.11  (*+*)Model_Pattern.to_string @{context} (MethodC.from_store ctxt mI' |> #model) = "[\"" ^