1.1 --- a/src/Tools/isac/Specify/refine.sml	Tue Jun 21 16:04:43 2022 +0200
     1.2 +++ b/src/Tools/isac/Specify/refine.sml	Wed Jun 22 16:24:08 2022 +0200
     1.3 @@ -37,23 +37,25 @@
     1.4  
     1.5  fun eq1 d (_, (d', _)) = (d = d');
     1.6  
     1.7 +(*  chk_: theory -> ('a * (term * term)) list -> I_Model.single -> I_Model.single*)
     1.8  fun chk_ (_: theory) pbt (i, vats, b, f, I_Model.Cor ((d, vs), _)) =
     1.9        (case find_first (eq1 d) pbt of 
    1.10 -        SOME (_, (_, id)) => (i, vats, b, f, I_Model.Cor ((d, vs), (id, I_Model.pbl_ids' d vs)))
    1.11 +        SOME (_, (_, id)) => (i, vats, b, f, I_Model.Cor ((d, vs), (id, [Input_Descript.join'''' (d, vs)])))
    1.12        | NONE =>  (i, vats, false, f, I_Model.Sup (d, vs)))
    1.13    | chk_ _ pbt (i, vats, b, f, I_Model.Inc ((d, vs), _)) =
    1.14        (case find_first (eq1 d) pbt of 
    1.15 -        SOME (_, (_, id)) => (i, vats, b, f, I_Model.Cor ((d, vs), (id, I_Model.pbl_ids' d vs)))
    1.16 +        SOME (_, (_, id)) => (i, vats, b, f, I_Model.Cor ((d, vs), (id, [Input_Descript.join'''' (d, vs)])))
    1.17        | NONE => (i, vats, false, f, I_Model.Sup (d, vs)))
    1.18    | chk_ _ _ (itm as (_, _, _, _, I_Model.Syn _)) = itm
    1.19    | chk_ _ _ (itm as (_, _, _, _, I_Model.Typ _)) = itm
    1.20    | chk_ _ pbt (i, vats, b, f, I_Model.Sup (d, vs)) =
    1.21        (case find_first (eq1 d) pbt of 
    1.22 -        SOME (_, (_, id)) => (i, vats, b, f, I_Model.Cor ((d,vs), (id, I_Model.pbl_ids' d vs)))
    1.23 +        SOME (_, (_, id)) => (i, vats, b, f, I_Model.Cor ((d,vs), (id, [Input_Descript.join'''' (d, vs)])))
    1.24        | NONE => (i, vats, false, f, I_Model.Sup (d, vs)))
    1.25    | chk_ _ pbt (i, vats, _, f, I_Model.Mis (d, vs)) =
    1.26        (case find_first (eq1 d) pbt of
    1.27 -        SOME (_, _) => raise ERROR "chk_: ((i,vats,b,f,I_Model.Cor ((d,vs),(id, I_Model.pbl_ids' d vs))):itm)"
    1.28 +        SOME _ =>
    1.29 +          raise ERROR "chk_: ((i,vats,b,f,I_Model.Cor ((d,vs),(id, Input_Descript.join'''' d vs))):itm)"
    1.30        | NONE => (i, vats, false, f, I_Model.Sup (d, [vs])))
    1.31    | chk_ _ _ _ = raise ERROR "chk_: uncovered fun def.";
    1.32