1.1 --- a/src/Tools/isac/Specify/p-spec.sml	Thu Dec 07 17:16:22 2023 +0100
     1.2 +++ b/src/Tools/isac/Specify/p-spec.sml	Sun Dec 10 07:56:02 2023 +0100
     1.3 @@ -24,8 +24,8 @@
     1.4      int list * bool * Model_Def.m_field * (I_Model.feedback_POS * Position.T)
     1.5    val imodel2fstr: p_model list -> (string * TermC.as_string) list
     1.6    val is_e_ts: term list -> bool
     1.7 -  val itms2fstr: Proof.context -> I_Model.single -> string * string
     1.8 -  val par2fstr: I_Model.single -> string * TermC.as_string
     1.9 +  val itms2fstr: Proof.context -> I_Model.single_POS -> string * string
    1.10 +  val par2fstr: I_Model.single_POS -> string * TermC.as_string
    1.11    val unknown_expl: ThyC.id -> Model_Pattern.T -> (Model_Def.m_field * string) list -> I_Model.T_POS
    1.12  (*\----- from isac_test for Minisubpbl*)
    1.13  
    1.14 @@ -118,17 +118,14 @@
    1.15      let val itm = appl_add' dI oris model pbt selct;
    1.16      in appl_adds dI oris (add itm model) pbt ss end
    1.17  
    1.18 -fun par2fstr (_, _, _, f, I_Model.Par s) = (f, s)
    1.19 +fun par2fstr (_, _, _, f, (I_Model.Syn_POS s, _)) = (f, s)
    1.20    | par2fstr itm = raise ERROR ("par2fstr: called with " ^
    1.21 -    I_Model.single_to_string (ContextC.for_ERROR ()) itm)
    1.22 -fun itms2fstr _ (_, _, _, f, I_Model.Cor ((d, ts), _)) = (f, Input_Descript.join''' (d, ts))
    1.23 -  | itms2fstr _ (_, _, _, f, I_Model.Syn str) = (f, str)
    1.24 -  | itms2fstr _ (_, _, _, f, I_Model.Typ str) = (f, str)
    1.25 -  | itms2fstr _ (_, _, _, f, I_Model.Inc ((d, ts), _)) = (f, Input_Descript.join''' (d,ts))
    1.26 -  | itms2fstr _ (_, _, _, f, I_Model.Sup (d, ts)) = (f, Input_Descript.join''' (d, ts))
    1.27 -  | itms2fstr ctxt (_, _, _, f, I_Model.Mis (d, t)) = (f, UnparseC.term ctxt (d $ t))
    1.28 -  | itms2fstr ctxt (itm as (_, _, _, _, I_Model.Par _)) = 
    1.29 -    raise ERROR ("itms2fstr (" ^ I_Model.single_to_string ctxt itm ^ "): Par should be internal");
    1.30 +    I_Model.single_to_string_POS (ContextC.for_ERROR ()) itm)
    1.31 +
    1.32 +fun itms2fstr _ (_, _, _, f, (I_Model.Cor_POS (d, ts), _)) = (f, Input_Descript.join''' (d, ts))
    1.33 +  | itms2fstr _ (_, _, _, f, (I_Model.Syn_POS str, _)) = (f, str)
    1.34 +  | itms2fstr _ (_, _, _, f, (I_Model.Inc_POS (d, ts), _)) = (f, Input_Descript.join''' (d,ts))
    1.35 +  | itms2fstr _ (_, _, _, f, (I_Model.Sup_POS (d, ts), _)) = (f, Input_Descript.join''' (d, ts))
    1.36  
    1.37  fun imodel2fstr iitems = 
    1.38    let