diff -r 344eee0d80f7 -r e797d1bdfe37 src/Tools/isac/Specify/p-spec.sml
--- a/src/Tools/isac/Specify/p-spec.sml	Mon Dec 11 16:18:42 2023 +0100
+++ b/src/Tools/isac/Specify/p-spec.sml	Mon Dec 11 17:26:30 2023 +0100
@@ -3,7 +3,7 @@
    (c) due to copyright terms
 
 Major parts will be dropped at switch to Isabelle/PIDE.
-Thus the switch to I_Model.T_POS is prepared quick and dirty.
+Thus the switch to I_Model.T is prepared quick and dirty.
 *)
 
 signature PRESENTATION_SPECIFICATION =
@@ -15,18 +15,18 @@
     | Given of TermC.as_string list
     | Relate of TermC.as_string list
 
-  val appl_add': ThyC.id -> O_Model.T -> I_Model.T_POS -> Model_Pattern.T ->
-    string * TermC.as_string -> I_Model.single_POS
-  val appl_adds: ThyC.id -> O_Model.T -> I_Model.T_POS -> Model_Pattern.T ->
-    (Model_Def.m_field * TermC.as_string) list -> I_Model.T_POS
+  val appl_add': ThyC.id -> O_Model.T -> I_Model.T -> Model_Pattern.T ->
+    string * TermC.as_string -> I_Model.single
+  val appl_adds: ThyC.id -> O_Model.T -> I_Model.T -> Model_Pattern.T ->
+    (Model_Def.m_field * TermC.as_string) list -> I_Model.T
   val eq7: ''a * ''b -> ''a * (''b * 'c) -> bool
   val fstr2itm_: theory -> Model_Pattern.T -> Model_Def.m_field * string ->
-    int list * bool * Model_Def.m_field * (I_Model.feedback_POS * Position.T)
+    int list * bool * Model_Def.m_field * (I_Model.feedback * Position.T)
   val imodel2fstr: p_model list -> (string * TermC.as_string) list
   val is_e_ts: term list -> bool
-  val itms2fstr: Proof.context -> I_Model.single_POS -> string * string
-  val par2fstr: I_Model.single_POS -> string * TermC.as_string
-  val unknown_expl: ThyC.id -> Model_Pattern.T -> (Model_Def.m_field * string) list -> I_Model.T_POS
+  val itms2fstr: Proof.context -> I_Model.single -> string * string
+  val par2fstr: I_Model.single -> string * TermC.as_string
+  val unknown_expl: ThyC.id -> Model_Pattern.T -> (Model_Def.m_field * string) list -> I_Model.T
 (*\----- from isac_test for Minisubpbl*)
 
 \<^isac_test>\<open>
@@ -59,14 +59,14 @@
   | is_e_ts [Const (\<^const_name>\<open>Nil\<close>, _)] = true
   | is_e_ts _ = false;
 
-fun appl_add' dI oris (model: I_Model.T_POS) pbt (sel, ct) = 
+fun appl_add' dI oris (model: I_Model.T) pbt (sel, ct) = 
   let 
      val ctxt = Know_Store.get_via_last_thy dI |> Proof_Context.init_global;
   in
     (*/------------ replace by ParseC.term_position ------------------\*)
     case ParseC.term_opt ctxt ct of
     (*\------------ replace by ParseC.term_position ------------------/*)
-	    NONE => (0, [], false, sel, (I_Model.Syn_POS ct, Position.none))
+	    NONE => (0, [], false, sel, (I_Model.Syn ct, Position.none))
 	  | SOME t =>
 	    (case O_Model.contains ctxt sel oris t of
         ("", ori', all) =>
@@ -75,8 +75,8 @@
           | (msg,_) => raise ERROR ("P_Spec.appl_add': " ^ msg))
       | (_, (i, v, _, d, ts), _) =>
         if is_e_ts ts
-        then (i, v, false, sel, (I_Model.Inc_POS (d, ts), Position.none))
-        else (i, v, false, sel, (I_Model.Sup_POS (d, ts), Position.none)))
+        then (i, v, false, sel, (I_Model.Inc (d, ts), Position.none))
+        else (i, v, false, sel, (I_Model.Sup (d, ts), Position.none)))
    end
 
 (* generate preliminary itm_ from a string (with field "#Given" etc.) *)
@@ -88,15 +88,15 @@
     (*\------------ replace by ParseC.term_position ? ------------/*)
   in
     case topt of
-      NONE => ([], false, f, (I_Model.Syn_POS str, Position.none))
+      NONE => ([], false, f, (I_Model.Syn str, Position.none))
     | SOME ct => 
 	    let
 	      val (d, ts) = Input_Descript.split ct
 	      val popt = find_first (eq7 (f, d)) pbt
 	    in
 	      case popt of
-	        NONE => ([1](*??*), true(*??*), f, (I_Model.Sup_POS (d, ts), Position.none))
-	      | SOME (f, (d, id)) => ([1], true, f, (I_Model.Cor_POS (d, ts), Position.none))
+	        NONE => ([1](*??*), true(*??*), f, (I_Model.Sup (d, ts), Position.none))
+	      | SOME (f, (d, id)) => ([1], true, f, (I_Model.Cor (d, ts), Position.none))
 	    end
   end
 
@@ -109,23 +109,23 @@
   in map flattup2 its end
 
 fun eq_dsc ((_, _, _, _, (itm_, _)), (_, _, _, _, (iitm_, _))) =
-  (I_Model.descriptor_POS itm_ = I_Model.descriptor_POS iitm_)
-fun add itm (itms: I_Model.T_POS) = if member eq_dsc itms itm then itms else itms @ [itm] (* @ new itm *)
+  (I_Model.descriptor itm_ = I_Model.descriptor iitm_)
+fun add itm (itms: I_Model.T) = if member eq_dsc itms itm then itms else itms @ [itm] (* @ new itm *)
 fun appl_adds dI [] _ pbt selcts = unknown_expl dI pbt selcts
     (*already present itms in model are being overwritten*)
-  | appl_adds _ _ (model: I_Model.T_POS) _ [] = model
-  | appl_adds dI oris (model: I_Model.T_POS) pbt (selct :: ss) =
+  | appl_adds _ _ (model: I_Model.T) _ [] = model
+  | appl_adds dI oris (model: I_Model.T) pbt (selct :: ss) =
     let val itm = appl_add' dI oris model pbt selct;
     in appl_adds dI oris (add itm model) pbt ss end
 
-fun par2fstr (_, _, _, f, (I_Model.Syn_POS s, _)) = (f, s)
+fun par2fstr (_, _, _, f, (I_Model.Syn s, _)) = (f, s)
   | par2fstr itm = raise ERROR ("par2fstr: called with " ^
-    I_Model.single_to_string_POS (ContextC.for_ERROR ()) itm)
+    I_Model.single_to_string (ContextC.for_ERROR ()) itm)
 
-fun itms2fstr _ (_, _, _, f, (I_Model.Cor_POS (d, ts), _)) = (f, Input_Descript.join''' (d, ts))
-  | itms2fstr _ (_, _, _, f, (I_Model.Syn_POS str, _)) = (f, str)
-  | itms2fstr _ (_, _, _, f, (I_Model.Inc_POS (d, ts), _)) = (f, Input_Descript.join''' (d,ts))
-  | itms2fstr _ (_, _, _, f, (I_Model.Sup_POS (d, ts), _)) = (f, Input_Descript.join''' (d, ts))
+fun itms2fstr _ (_, _, _, f, (I_Model.Cor (d, ts), _)) = (f, Input_Descript.join''' (d, ts))
+  | itms2fstr _ (_, _, _, f, (I_Model.Syn str, _)) = (f, str)
+  | itms2fstr _ (_, _, _, f, (I_Model.Inc (d, ts), _)) = (f, Input_Descript.join''' (d,ts))
+  | itms2fstr _ (_, _, _, f, (I_Model.Sup (d, ts), _)) = (f, Input_Descript.join''' (d, ts))
 
 fun imodel2fstr iitems = 
   let