1.1 --- a/TODO.md	Sun Dec 10 07:56:02 2023 +0100
     1.2 +++ b/TODO.md	Sun Dec 10 17:35:07 2023 +0100
     1.3 @@ -47,8 +47,8 @@
     1.4  * WN: 
     1.5  * WN: clarify handling "#undef" -> type m_field  +++  bool in i_single
     1.6     ?RN?or?just for OLD? ori_2itm -> single_from_o, ori_2itm_POS -> single_from_o_POS
     1.7 -* WN: replace I_Model.values_POS' -> val get_values = Pre_Conds.get_values
     1.8 -* WN: RN o_model_values -> get_values, values_POS' -> get_values_POS, 
     1.9 +* WN: replace I_Model.feedb_values -> val get_values = Pre_Conds.get_values
    1.10 +* WN: RN o_model_values -> get_values, feedb_values -> get_values_POS, 
    1.11     TEST_to_OLD -> POS_to_OLD, TEST_to_OLD_single -> POS_to_OLD_single,
    1.12     
    1.13  * WN: eliminate max_variant in favour of max_variants

     2.1 --- a/src/Tools/isac/BridgeJEdit/preliminary.sml	Sun Dec 10 07:56:02 2023 +0100
     2.2 +++ b/src/Tools/isac/BridgeJEdit/preliminary.sml	Sun Dec 10 17:35:07 2023 +0100
     2.3 @@ -7,7 +7,7 @@
     2.4  
     2.5  signature PRELIMINARY =
     2.6  sig
     2.7 -  val check_input: Model_Pattern.model_input_pos -> I_Model.T
     2.8 +  val check_input: Model_Pattern.model_input_pos -> I_Model.T_POS
     2.9    val init_ctree: theory -> string -> CTbasic_POS.ctree
    2.10    val update_state: theory -> string * (Model_Pattern.model_input_pos * References.input) ->
    2.11      CTbasic_POS.ctree -> CTbasic_POS.ctree
    2.12 @@ -25,7 +25,7 @@
    2.13   * parse_references_input works
    2.14   * switching \<Odot>\<Otimes> i_model for probl and meth works.
    2.15  *)
    2.16 -fun check_input (*ctxt o-model ??*) (_: Model_Pattern.model_input_pos) = []: I_Model.T (*TODO*)
    2.17 +fun check_input (*ctxt o-model ??*) (_: Model_Pattern.model_input_pos) = []: I_Model.T_POS (*TODO*)
    2.18  (** first trial: init or update state **)
    2.19  
    2.20  (* at the first encounter of an Example create the following data and transfer them to ctree:

     3.1 --- a/src/Tools/isac/Build_Isac.thy	Sun Dec 10 07:56:02 2023 +0100
     3.2 +++ b/src/Tools/isac/Build_Isac.thy	Sun Dec 10 17:35:07 2023 +0100
     3.3 @@ -165,8 +165,6 @@
     3.4  (*\\-----------------------------------------------------------------------------------------//*)
     3.5  begin
     3.6  ML \<open>
     3.7 -(** )
     3.8 -( **)
     3.9  \<close> ML \<open>
    3.10  
    3.11  \<close> ML \<open>

     4.1 --- a/src/Tools/isac/Interpret/li-tool.sml	Sun Dec 10 07:56:02 2023 +0100
     4.2 +++ b/src/Tools/isac/Interpret/li-tool.sml	Sun Dec 10 17:35:07 2023 +0100
     4.3 @@ -27,11 +27,9 @@
     4.4    val tac_from_prog: Ctree.state -> term -> Tactic.input
     4.5  
     4.6  (*from isac_test for Minisubpbl*)
     4.7 -  val arguments_from_model : Proof.context -> MethodC.id -> I_Model.T -> term list
     4.8 +  val arguments_from_model: Proof.context -> MethodC.id -> I_Model.T_POS -> term list
     4.9    val errmsg: string
    4.10 -  val error_msg_2: Proof.context -> term -> I_Model.T -> string
    4.11 -  val error_msg_2_POS: Proof.context -> term -> I_Model.T_POS -> string
    4.12 -  val error_msg_1: string
    4.13 +  val error_msg: string
    4.14    val relate_args: Env.T -> term list -> term list -> Proof.context -> Program.term ->
    4.15      MethodC.id -> term list -> term list -> (term * term) list
    4.16  
    4.17 @@ -57,24 +55,19 @@
    4.18      Option.map (subst_atomic env) (Prog_Tac.get_first_argument prog)
    4.19    | implicit_take _ _ _ = raise ERROR "implicit_take: no match";
    4.20  
    4.21 -val error_msg_1 = "ERROR: the guard is missing (#model in 'type met' added in prep_met)."
    4.22 -fun error_msg_2 ctxt d itms =
    4.23 -  ("arguments_from_model: '" ^ UnparseC.term ctxt d ^ "' not in itms:\n" ^
    4.24 -  "itms:\n" ^ I_Model.to_string @{context} itms)
    4.25 -fun error_msg_2_POS ctxt d itms =
    4.26 -  ("arguments_from_model: '" ^ UnparseC.term ctxt d ^ "' not in itms:\n" ^
    4.27 -  "itms:\n" ^ I_Model.to_string_POS @{context} itms)
    4.28 +val error_msg = "ERROR: the guard is missing (#model in 'type met' added in prep_met)."
    4.29  (* turn Model-items into arguments for a program *)
    4.30 -fun arguments_from_model ctxt mI itms =
    4.31 +fun arguments_from_model ctxt met_id i_model =
    4.32    let
    4.33 -    val mvat = Pre_Conds.max_variant itms
    4.34 -    fun okv mvat (_, vats, b, _, _) = member op = vats mvat andalso b
    4.35 -    val itms = filter (okv mvat) itms
    4.36 -    fun itm2arg _ (_, (_, _)) = [](*this limits errors to init_pstate,
    4.37 -      while changing I_Model.penvval_in triggers much more errors*)
    4.38 -    val pats = (#model o MethodC.from_store ctxt) mI
    4.39 -    val _ = if pats = [] then raise ERROR error_msg_1 else ()
    4.40 -  in (flat o (map (itm2arg itms))) pats end;
    4.41 +    val {model = met_patt, ...} = MethodC.from_store ctxt met_id
    4.42 +    val max_vnt = Model_Def.max_variants'' i_model |> last_elem
    4.43 +  in
    4.44 +    i_model
    4.45 +      |> filter (fn (_, vnts, _, _, _) => member_swap op = max_vnt vnts)
    4.46 +      |> I_Model.order_by_patt met_patt
    4.47 +      |> I_Model.get_values
    4.48 +      |> map Model_Def.values_to_present
    4.49 +  end
    4.50  
    4.51  (*
    4.52    convert a Prog_Tac to Tactic.input;

     5.1 --- a/src/Tools/isac/Knowledge/Biegelinie.thy	Sun Dec 10 07:56:02 2023 +0100
     5.2 +++ b/src/Tools/isac/Knowledge/Biegelinie.thy	Sun Dec 10 17:35:07 2023 +0100
     5.3 @@ -113,7 +113,7 @@
     5.4    E.g. for "Traegerlaenge" in the problem we had "l_l", while in the method we had "beam".
     5.5    This had been working with the old "fun arguments_from_model, relate_args" in LItool.
     5.6    But the Pre_Conds of Biegelinie were empty at that time --
     5.7 -  -- how should this work with Pre_Conds <>[] involved with both, problem and method?
     5.8 +  -- how should this work with Pre_Conds <> [] involved with both, problem and method?
     5.9    A kind of "model-translation" (see the old "fun LItool.arguments_from_model";
    5.10    there is already an implicit kind of relation exploitet by refinement)?
    5.11    In this changeset there is the decision to make the two models equal, of model and of method.
    5.12 @@ -345,7 +345,7 @@
    5.13      "FunktionsVariable fun_var" "AbleitungBiegelinie id_der" "Biegemoment id_momentum"
    5.14      "Querkraft id_lat_force"
    5.15    (* Item for Problem "LINEAR/system", which by [''no_met''] involves refinement *)
    5.16 -    "GleichungsVariablen vs"(*NEW*)
    5.17 +    "GleichungsVariablen vs"
    5.18    Find: "Biegelinie b_b"
    5.19  
    5.20  method met_biege_intconst_2 : "IntegrierenUndKonstanteBestimmen/2xIntegrieren" =

     6.1 --- a/src/Tools/isac/Knowledge/Test.thy	Sun Dec 10 07:56:02 2023 +0100
     6.2 +++ b/src/Tools/isac/Knowledge/Test.thy	Sun Dec 10 17:35:07 2023 +0100
     6.3 @@ -813,8 +813,7 @@
     6.4          [\<^rule_eval>\<open>contains_root\<close> (eval_contains_root "")],
     6.5      where_rls = Rule_Set.append_rules "prls_contains_root" Rule_Set.empty 
     6.6          [\<^rule_eval>\<open>contains_root\<close> (eval_contains_root "")],
     6.7 -    calc=[],errpats = [], rew_rls = Rule_Set.empty (*,asm_rls=[],
     6.8 -    asm_thm=[("square_equation_left", ""), ("square_equation_right", "")]*)}\<close>
     6.9 +    calc = [], errpats = [], rew_rls = Rule_Set.empty}\<close>
    6.10    Program: solve_root_equ.simps
    6.11    Given: "equality e_e" "solveFor v_v"
    6.12    Where: "contains_root (e_e::bool)"

     7.1 --- a/src/Tools/isac/MathEngBasic/model-def.sml	Sun Dec 10 07:56:02 2023 +0100
     7.2 +++ b/src/Tools/isac/MathEngBasic/model-def.sml	Sun Dec 10 17:35:07 2023 +0100
     7.3 @@ -93,8 +93,8 @@
     7.4  (3) solveForVars    [c, c_2, c_3]     [[  [c], [c_2], [c_3]   ]]   [[  [c], [c_2], [c_3]   ]]
     7.5  (4) Constants       [r = 7]           [[  [[r = 7]]           ]]   [[  [[r = 7]]           ]]
     7.6  (5) Maximum         A                 [[  A                   ]]   [[  A                   ]]
     7.7 -                              ---> fun make_values (descr, ts) -->
     7.8 -                              <--- fun make_present (descr, ts) <--
     7.9 +                            ---> Model_Def.make_values (descr, ts) -->
    7.10 +                        <--- Model_Def.values_to_present ctxt (descr, ts) <--
    7.11  
    7.12  Observe the elements of HOL-lists enclosed in ML-lists in lines (2..4).
    7.13  Without those (strange!) HOL-lists in values one could not distinguish (1) and (3), 

     8.1 --- a/src/Tools/isac/Specify/i-model.sml	Sun Dec 10 07:56:02 2023 +0100
     8.2 +++ b/src/Tools/isac/Specify/i-model.sml	Sun Dec 10 17:35:07 2023 +0100
     8.3 @@ -50,7 +50,6 @@
     8.4    val init_POS: Proof.context -> O_Model.T -> Model_Pattern.T -> T_POS
     8.5    val check_single: Proof.context -> m_field -> O_Model.T -> T -> Model_Pattern.T ->
     8.6      TermC.as_string -> add_single
     8.7 -  (*probably unused in PIDE, thus-----v----v*)
     8.8    val add_single: theory -> single_POS -> T_POS -> T_POS
     8.9  
    8.10    val make_tactic: m_field -> TermC.as_string * T_POS -> Tactic.T
    8.11 @@ -58,8 +57,10 @@
    8.12    val descriptor: feedback -> descriptor
    8.13    val descriptor_POS: feedback_POS -> descriptor
    8.14    val values: feedback -> values option
    8.15 +  val get_values: T_POS -> values list
    8.16    val o_model_values: feedback -> values
    8.17 -  val values_POS': feedback_POS -> values
    8.18 +  val feedb_values: feedback_POS -> values
    8.19 +  val order_by_patt:  Model_Pattern.T -> T_POS ->T_POS
    8.20    val descr_pairs_to_string: Proof.context -> (Model_Pattern.single * single_POS) list -> string
    8.21    val variables: Model_Pattern.T -> Model_Def.i_model_POS -> term list
    8.22    val is_notyet_input: Proof.context -> T_POS -> O_Model.values -> O_Model.single ->
    8.23 @@ -275,10 +276,28 @@
    8.24    | o_model_values (Sup (_, ts)) = ts
    8.25    | o_model_values (Mis _) = []
    8.26    | o_model_values _ = raise ERROR "o_model_values: uncovered case in fun.def.";
    8.27 -fun values_POS' (Cor_POS (_, ts)) = ts
    8.28 -  | values_POS' (Syn_POS _) = raise ERROR "values_POS' NOT for Syn_POS"
    8.29 -  | values_POS' (Inc_POS (_, ts)) = ts
    8.30 -  | values_POS' (Sup_POS (_, ts)) = ts
    8.31 +(*RN feedb_vals'*)
    8.32 +fun feedb_values (Cor_POS (_, ts)) = ts
    8.33 +  | feedb_values (Syn_POS _) = raise ERROR "feedb_values NOT for Syn_POS"
    8.34 +  | feedb_values (Inc_POS (_, ts)) = ts
    8.35 +  | feedb_values (Sup_POS (_, ts)) = ts
    8.36 +
    8.37 +(*assumption: i_model has filtered max_vnt*)
    8.38 +local
    8.39 + fun order_by_pa i_model (_, (descr, _ )) =
    8.40 +   case find_first (fn (_, _, _, _, (feedb, _)) => descr = descriptor_POS feedb) i_model of
    8.41 +     SOME i_single => [i_single]
    8.42 +   | NONE => []
    8.43 +in
    8.44 +  fun order_by_patt model_patt i_model = model_patt |> map (order_by_pa i_model) |> flat
    8.45 +end
    8.46 +fun feedb_vals (Cor_POS (_, ts)) = [ts]
    8.47 +  | feedb_vals (Syn_POS _) = []
    8.48 +  | feedb_vals (Inc_POS (_, ts)) = [ts]
    8.49 +  | feedb_vals (Sup_POS (_, ts)) = [ts]
    8.50 +fun get_values i_model =
    8.51 +  map (fn (_, _, _, _, (feedb, _)) => feedb_vals feedb) i_model
    8.52 +  |> flat
    8.53  
    8.54  fun descr_pairs_to_string ctxt equal_descr_pairs =
    8.55  (map (fn (a, b) => pair (Model_Pattern.single_to_string ctxt a) (single_to_string_POS ctxt b)
    8.56 @@ -301,7 +320,7 @@
    8.57  (*update the itm_ already input, all..from ori*)
    8.58  fun ori_2itm (feedb:feedback_POS) _ all (id, vt, fd, d, ts) = 
    8.59    let 
    8.60 -    val ts' = union op = (values_POS' feedb) ts;
    8.61 +    val ts' = union op = (feedb_values feedb) ts;
    8.62      val complete = if eq_set op = (ts', all) then true else false
    8.63    in
    8.64      case feedb of
    8.65 @@ -327,7 +346,7 @@
    8.66            f = f' andalso d = (descriptor_POS feedb)) itms of
    8.67          SOME (_, _, _, _, (feedb, _)) =>
    8.68            let
    8.69 -            val ts' = inter op = (values_POS' feedb) ts
    8.70 +            val ts' = inter op = (feedb_values feedb) ts
    8.71            in
    8.72              if subset op = (ts, ts') 
    8.73              then (((strs2str' o map (UnparseC.term ctxt)) ts') ^ " already input", empty_single_POS)
    8.74 @@ -473,7 +492,7 @@
    8.75      if Model_Def.is_list_descr descr
    8.76      then
    8.77        let
    8.78 -        val already_input = feedb |> values_POS'
    8.79 +        val already_input = feedb |> feedb_values
    8.80          val miss = subtract op= already_input all_values (*"[[c], [c_2], [c_3], [c_4]]"*)
    8.81          val ts = already_input @ [hd miss]
    8.82        in

     9.1 --- a/src/Tools/isac/Specify/specify.sml	Sun Dec 10 07:56:02 2023 +0100
     9.2 +++ b/src/Tools/isac/Specify/specify.sml	Sun Dec 10 17:35:07 2023 +0100
     9.3 @@ -12,13 +12,10 @@
     9.4    val by_Add_: string -> TermC.as_string -> Calc.T -> string * Calc.state_post
     9.5  
     9.6  (*from isac_test for Minisubpbl*)
     9.7 -(*OLD*)
     9.8    val for_problem: Proof.context -> O_Model.T -> References.T * References.T -> I_Model.T_POS * I_Model.T_POS ->
     9.9      string * (Pos.pos_ * Tactic.input)
    9.10    val for_method: Proof.context -> O_Model.T -> References.T * References.T -> I_Model.T_POS * I_Model.T_POS ->
    9.11      string * (Pos.pos_ * Tactic.input)
    9.12 -(*---*)
    9.13 -(*NEW*)
    9.14    val select_inc_lists: I_Model.T_POS -> I_Model.T_POS
    9.15  
    9.16  \<^isac_test>\<open>

    10.1 --- a/src/Tools/isac/Test_Code/Test_Code.thy	Sun Dec 10 07:56:02 2023 +0100
    10.2 +++ b/src/Tools/isac/Test_Code/Test_Code.thy	Sun Dec 10 17:35:07 2023 +0100
    10.3 @@ -14,7 +14,7 @@
    10.4  
    10.5  ML \<open>
    10.6  \<close> ML \<open>
    10.7 -ThyC.get_theory
    10.8 +
    10.9  \<close> ML \<open>
   10.10  \<close>
   10.11  end

    11.1 --- a/test/Tools/isac/Interpret/error-pattern.sml	Sun Dec 10 07:56:02 2023 +0100
    11.2 +++ b/test/Tools/isac/Interpret/error-pattern.sml	Sun Dec 10 17:35:07 2023 +0100
    11.3 @@ -1318,7 +1318,7 @@
    11.4     ...vvv
    11.5     *)
    11.6  (* val (dI, oris, model, pbt, (selct::ss))=
    11.7 -       (#1 (References.select_input ospec spec), oris, []:I_Model.T,
    11.8 +       (#1 (References.select_input ospec spec), oris, []:I_Model.T_POS,
    11.9  	((#model o Problem.from_store) (#2 (References.select_input ospec spec))),(imodel2fstr imodel));
   11.10     val iii = appl_adds dI oris model pbt (selct::ss); 
   11.11     tracing(I_Model.to_string thy iii);

    12.1 --- a/test/Tools/isac/Interpret/li-tool.sml	Sun Dec 10 07:56:02 2023 +0100
    12.2 +++ b/test/Tools/isac/Interpret/li-tool.sml	Sun Dec 10 17:35:07 2023 +0100
    12.3 @@ -12,7 +12,7 @@
    12.4  "----------- fun go ----------------------------------------------";
    12.5  "----------- fun formal_args -------------------------------------";
    12.6  "----------- fun dsc_valT ----------------------------------------";
    12.7 -"----------- fun arguments_from_model ---------------------------------------";
    12.8 +"----------- fun arguments_from_model --------------------------------------------------------";
    12.9  "----------- fun init_pstate -----------------------------------------------------------------";
   12.10  "-----------------------------------------------------------------";
   12.11  "-----------------------------------------------------------------";
   12.12 @@ -229,17 +229,42 @@
   12.13  > val dsc = dsc_valT t;
   12.14  val dsc = "nam" : string*)
   12.15  
   12.16 -(** -------- fun arguments_from_model ------------------------------------- **)
   12.17 -"----------- fun arguments_from_model ---------------------------------------";
   12.18 -"----------- fun arguments_from_model ---------------------------------------";
   12.19 -(*
   12.20 -> val sc = ... Solve_root_equation ...
   12.21 -> val mI = ("Program", "sqrt-equ-test");
   12.22 -> val PblObj{meth={model=itms,...},...} = get_obj I pt [];
   12.23 -> val ts = arguments_from_model thy mI itms;
   12.24 -> map (UnparseC.term_in_thy thy) ts;
   12.25 -["sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x)", "x", "#0"] : string list
   12.26 -*)
   12.27 +(** -------- fun arguments_from_model ------------------------------------------------------ **)
   12.28 +"----------- fun arguments_from_model --------------------------------------------------------";
   12.29 +"----------- fun arguments_from_model --------------------------------------------------------";
   12.30 +val ctxt = @{context}
   12.31 +val {program = Prog prog, ...} = MethodC.from_store ctxt ["IntegrierenUndKonstanteBestimmen2"]
   12.32 +val f_model: term list = map (ParseC.parse_test ctxt) [
   12.33 +  "Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",
   12.34 +	 "Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]",
   12.35 +	 "FunktionsVariable x",
   12.36 +   "AbleitungBiegelinie y'",
   12.37 +   "Biegemoment M_b",
   12.38 +   "Querkraft Q",
   12.39 +   "GleichungsVariablen [c, c_2, c_3, c_4]"];
   12.40 +
   12.41 +val descr_ts = f_model |> map (fn (descr $ term) => (descr, term))
   12.42 +val descr_valss = map (fn (descr, term) => (descr, make_values (descr, term))) descr_ts
   12.43 +val i_model_test: I_Model.T_POS = map
   12.44 +  (fn descr_vals => (4711, [1], true, "#undef", (Cor_POS descr_vals, Position.none))) descr_valss
   12.45 +
   12.46 +val return_arguments_from_model =
   12.47 +    LItool.arguments_from_model ctxt ["IntegrierenUndKonstanteBestimmen2"] i_model_test;
   12.48 +"~~~~~ fun arguments_from_model , args:"; val (ctxt, met_id, i_model) =
   12.49 +  (@{context}, ["IntegrierenUndKonstanteBestimmen2"], i_model_test)
   12.50 +    val {model = met_patt, ...} = MethodC.from_store ctxt met_id
   12.51 +    val max_vnt = Model_Def.max_variants'' i_model |> last_elem
   12.52 +val return_arguments_from_model_STEP = i_model
   12.53 +      |> filter (fn (_, vnts, _, _, _) => member_swap op = max_vnt vnts)
   12.54 +      |> order_by_patt met_patt
   12.55 +      |> get_values
   12.56 +      |> map values_to_present
   12.57 +
   12.58 +(*+*)val   "[L, q_0, [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0], x, y', M_b, Q, [c, c_2, c_3, c_4], y]"
   12.59 +  = return_arguments_from_model_STEP |> UnparseC.terms ctxt
   12.60 +(*^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ new version equals old version vvvvvvvvvvvvvvvvvvvvvvvvvvvvvvv*)
   12.61 +(*+* ) val "[L, q_0, [M_b 0 = 0, y 0 = 0, y L = 0, M_b L = 0], x, y', M_b, Q, [c_3, c, c_2, c_4], y]"
   12.62 +  = actuals |> UnparseC.terms ctxt( *+*)
   12.63  ;
   12.64  
   12.65  (** -------- fun init_pstate --------------------------------------------------------------- **);
   12.66 @@ -259,17 +284,13 @@
   12.67    since ROOT MethodC must provide values for "actuals" of ALL SubProblems.
   12.68    See Biegelinie.thy subsection \<open>Survey on Methods\<close>.
   12.69  *)
   12.70 -(*
   12.71 -  Items for MethodC "IntegrierenUndKonstanteBestimmen2"
   12.72 -*)
   12.73 +(*Items for MethodC "IntegrierenUndKonstanteBestimmen2"*)
   12.74  	    "FunktionsVariable x",
   12.75      (*"Biegelinie y",          ..already input for Problem above*)
   12.76        "AbleitungBiegelinie y'",
   12.77        "Biegemoment M_b",
   12.78        "Querkraft Q",
   12.79 -(*
   12.80 -  Item for Problem "LINEAR/system", which by [''no_met''] involves refinement
   12.81 -*)
   12.82 +(*Item for Problem "LINEAR/system", which by [''no_met''] involves refinement*)
   12.83        "GleichungsVariablen [c, c_2, c_3, c_4]"
   12.84  ];
   12.85  val (dI',pI',mI') = ("Biegelinie", ["Biegelinien"],

    13.1 --- a/test/Tools/isac/Minisubpbl/100a-init-rootpbl-Maximum.sml	Sun Dec 10 07:56:02 2023 +0100
    13.2 +++ b/test/Tools/isac/Minisubpbl/100a-init-rootpbl-Maximum.sml	Sun Dec 10 17:35:07 2023 +0100
    13.3 @@ -364,7 +364,7 @@
    13.4  val SOME (_, _, _, _, (feedb, _)) =
    13.5      (*case*) find_first (fn (_, _, _, f', (feedb, _)) =>
    13.6            f = f' andalso d = (descriptor_POS feedb)) itms
    13.7 -            val ts' = inter op = (values_POS' feedb) ts
    13.8 +            val ts' = inter op = (feedb_values feedb) ts
    13.9  val false =
   13.10              (*if*) subset op = (ts, ts') 
   13.11  
   13.12 @@ -372,7 +372,7 @@
   13.13             ori_2itm feedb pid all (i, v, f, d, subtract op = ts' ts));
   13.14  "~~~~~ fun ori_2itm , args:"; val (feedb, pid, all, (id, vt, fd, d, ts)) =
   13.15    (feedb, pid, all, (i, v, f, d, subtract op = ts' ts));
   13.16 -    val ts' = union op = (values_POS' feedb) ts;
   13.17 +    val ts' = union op = (feedb_values feedb) ts;
   13.18      val pval = [Input_Descript.join'''' (d, ts')]
   13.19      val complete = if eq_set op = (ts', all) then true else false
   13.20  

    14.1 --- a/test/Tools/isac/Specify/i-model.sml	Sun Dec 10 07:56:02 2023 +0100
    14.2 +++ b/test/Tools/isac/Specify/i-model.sml	Sun Dec 10 17:35:07 2023 +0100
    14.3 @@ -781,7 +781,7 @@
    14.4      (*in*)
    14.5  val true =
    14.6      (*if*) Model_Def.is_list_descr descr
    14.7 -        val already_input as [Const ("List.list.Cons", _) $ Free ("v", _) $ _] = feedb |> values_POS'
    14.8 +        val already_input as [Const ("List.list.Cons", _) $ Free ("v", _) $ _] = feedb |> feedb_values
    14.9  
   14.10          val miss = subtract op= already_input all_value
   14.11  (*+*)val "[[u]]" = miss |> UnparseC.terms ctxt

    15.1 --- a/test/Tools/isac/Specify/pre-conditions.sml	Sun Dec 10 07:56:02 2023 +0100
    15.2 +++ b/test/Tools/isac/Specify/pre-conditions.sml	Sun Dec 10 17:35:07 2023 +0100
    15.3 @@ -45,7 +45,7 @@
    15.4    (5, [1,2], true, "#Relate",
    15.5      (Cor_POS ((@{term "SideConditions"}, [@{term "[(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]"}])), Position.none ))
    15.6    :: [] : I_Model.T_POS;
    15.7 -val probl_OLD = I_Model.TEST_to_OLD probl : I_Model.T;
    15.8 +val probl_OLD = probl
    15.9  
   15.10  val {model = model_patt, where_rls, where_ = where_OLD, ...} = (*from_store without Position.T-vv*)
   15.11    Problem.from_store ctxt (References.explode_id "univariate_calculus/Optimisation")

    16.1 --- a/test/Tools/isac/Test_Theory.thy	Sun Dec 10 07:56:02 2023 +0100
    16.2 +++ b/test/Tools/isac/Test_Theory.thy	Sun Dec 10 17:35:07 2023 +0100
    16.3 @@ -206,9 +206,9 @@
    16.4  \<close> ML \<open>
    16.5  \<close>
    16.6  
    16.7 -(**)ML_file "Specify/i-model.sml"(**)
    16.8 +(**)ML_file "Interpret/li-tool.sml"(**)
    16.9  section \<open>===================================================================================\<close>
   16.10 -section \<open>===== new code xxxxx ==============================================================\<close>
   16.11 +section \<open>=====  ============================================================================\<close>
   16.12  ML \<open>
   16.13  \<close> ML \<open>
   16.14