1.1 --- a/src/Tools/isac/Specify/model.sml	Sat May 09 13:15:25 2020 +0200
     1.2 +++ b/src/Tools/isac/Specify/model.sml	Sat May 09 15:31:15 2020 +0200
     1.3 @@ -18,7 +18,6 @@
     1.4      With: string list} -> string
     1.5    val itemppc2str : item ppc -> string
     1.6  
     1.7 -  val pbl_ids' : term -> term list -> term list
     1.8    val mkval' : term list -> term
     1.9  
    1.10  (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
    1.11 @@ -36,10 +35,10 @@
    1.12    (1.1) untouched: for modeling only dsc displayed(impossible after match_itms)
    1.13          =(presently) Mis (? should be Inc initially, and Mis after match_itms?)
    1.14    (1.2)  Syn,Typ,Sup: not related to oris
    1.15 -    Syn, Typ (presently) should be accepted in appl_add (instead Error')
    1.16 -    Sup      (presently) should be accepted in appl_add (instead Error')
    1.17 +    Syn, Typ (presently) should be accepted in I_Model.add_single (instead Error')
    1.18 +    Sup      (presently) should be accepted in I_Model.add_single (instead Error')
    1.19           _could_ be w.r.t current vat (and then _is_ related to vat
    1.20 -    Mis should _not_ be  made Inc ((presently, by appl_add & match_itms)
    1.21 +    Mis should _not_ be  made Inc ((presently, by I_Model.add_single & match_itms)
    1.22  - dsc in I_Model.feedback is timeconsuming -- keep id for respective queries ?
    1.23  - order of items in ppc should be stable w.r.t order of itms
    1.24  
    1.25 @@ -77,9 +76,6 @@
    1.26    | mkval _ ts = TermC.list2isalist ((type_of o hd) ts) ts;
    1.27  fun mkval' x = mkval TermC.empty x;
    1.28  
    1.29 -(* 9.5.03 penv postponed: pbl_ids' *)
    1.30 -fun pbl_ids' d vs = [Input_Descript.join'''' (d, vs)];
    1.31 -
    1.32  (* for _output_ of the items of a Model *)
    1.33  datatype item = 
    1.34      Correct of TermC.as_string (* labels a correct formula (type cterm') *)