diff -r ac0317936138 -r 439e23525491 test/Tools/isac/Minisubpbl/100a-init-rootpbl-Maximum.sml
--- a/test/Tools/isac/Minisubpbl/100a-init-rootpbl-Maximum.sml	Tue Dec 05 18:15:45 2023 +0100
+++ b/test/Tools/isac/Minisubpbl/100a-init-rootpbl-Maximum.sml	Thu Dec 07 11:54:42 2023 +0100
@@ -325,7 +325,7 @@
            (if pI = Problem.id_empty then pI' else pI) |> Problem.from_store ctxt |> #model);
 
       (*case*)
-   I_Model.check_single ctxt m_field oris i_model m_patt ct (*of*);
+   I_Model.check_single ctxt m_field oris (I_Model.TEST_to_OLD i_model) m_patt ct (*of*);
 "~~~~~ fun check_single , args:"; val (ctxt, m_field, o_model, i_model, m_patt, (str(*, pos*))) =
   (ctxt, m_field, oris, i_model, m_patt, ct);
         val (t as (descriptor $ _)) = Syntax.read_term ctxt str
@@ -360,21 +360,23 @@
 "~~~~~ fun is_notyet_input , args:"; val (ctxt, itms, all, (i, v, f, d, ts), pbt) =
   (ctxt, i_model, all, ori', m_patt);
 val SOME (_, (_, pid)) =
-  (*case*) find_first (eq1 d) pbt (*of*);
-(*local*)fun eq3 f d (_, _, _, f', itm_) = f = f' andalso d = (I_Model.descriptor itm_);(*local*)
-val SOME (_, _, _, _, itm_) =
-    (*case*) find_first (eq3 f d) itms (*of*);
-val ts' = inter op = (o_model_values itm_) ts;
-            (*if*) subset op = (ts, ts') (*else*);
-val return_is_notyet_input = ("", 
-           ori_2itm itm_ pid all (i, v, f, d, subtract op = ts' ts));
-"~~~~~ fun ori_2itm , args:"; val (itm_, pid, all, (id, vt, fd, d, ts)) =
-  (itm_, pid, all, (i, v, f, d, subtract op = ts' ts));
-    val ts' = union op = (o_model_values itm_) ts;
+  (*case*) find_first (fn (_, (d', _)) => d = d') pbt
+val SOME (_, _, _, _, (feedb, _)) =
+    (*case*) find_first (fn (_, _, _, f', (feedb, _)) =>
+          f = f' andalso d = (descriptor_POS feedb)) itms
+            val ts' = inter op = (values_POS' feedb) ts
+val false =
+            (*if*) subset op = (ts, ts') 
+
+val return_is_notyet_input = ("",
+           ori_2itm feedb pid all (i, v, f, d, subtract op = ts' ts));
+"~~~~~ fun ori_2itm , args:"; val (feedb, pid, all, (id, vt, fd, d, ts)) =
+  (feedb, pid, all, (i, v, f, d, subtract op = ts' ts));
+    val ts' = union op = (values_POS' feedb) ts;
     val pval = [Input_Descript.join'''' (d, ts')]
     val complete = if eq_set op = (ts', all) then true else false
 
-(*+*)val "Inc Constants [] , pen2str" = itm_ |> I_Model.feedback_to_string ctxt
+(*+*)val "Inc_POS Constants [] [__=__, __=__]" = feedb |> I_Model.feedback_POS_to_string ctxt
 (*\\\----------------- step into specify_do_next -------------------------------------------//*)
 (*\\------------------ step into do_next ---------------------------------------------------//*)
 val ("ok", (ts as (_, _, _) :: _, _, (pt, p))) = return_do_next
@@ -400,7 +402,9 @@
   Pbl(*Frm,Pbl*)) = (ppobj, p_);
       val (_, _, met_id) = References.select_input o_spec spec
       val (allcorr, _) = Pre_Conds.check_internal ctxt (I_Model.OLD_to_POS probl) (Pos.Met, met_id)
-val return_pt_model = Ctree.ModSpec (allcorr, Pos.Pbl, hdl, probl, (*where_*)[(*Problem.from_store in check*)], spec)
+
+val return_pt_model = Ctree.ModSpec (allcorr, Pos.Pbl, hdl, I_Model.OLD_to_POS probl,
+  (*where_*)[(*Problem.from_store in check*)], spec)
 
 (*|------------------- continue with TESTg_form ----------------------------------------------*)
 val Ctree.ModSpec (spec as (_, p_, _, gfr, where_, _)) =
@@ -414,9 +418,9 @@
       | coll model ((_, _, _, field, itm_) :: itms) =
         coll (add_sel_ppc thy field model (item_from_feedback thy itm_)) itms;
 
- val gfr = coll P_Model.empty itms;
+ val gfr = coll P_Model.empty (I_Model.TEST_to_OLD itms);
 "~~~~~ fun coll , args:"; val (model, ((aaa, bbb_,ccc_, field, itm_) :: itms))
-  = (P_Model.empty, itms);
+  = (P_Model.empty, I_Model.TEST_to_OLD  itms);
 
 (*+*)val 4 = length itms;
 (*+*)val itm = nth 1 itms;