1.1 --- a/src/Tools/isac/Specify/p-spec.sml	Mon Jun 20 11:55:55 2022 +0200
     1.2 +++ b/src/Tools/isac/Specify/p-spec.sml	Mon Jun 20 18:37:54 2022 +0200
     1.3 @@ -143,7 +143,7 @@
     1.4      case TermC.parseNEW ctxt ct of
     1.5  	    NONE => (0, [], false, sel, I_Model.Syn ct)
     1.6  	  | SOME t =>
     1.7 -	    (case O_Model.is_known ctxt sel oris t of
     1.8 +	    (case O_Model.contains ctxt sel oris t of
     1.9          ("", ori', all) =>
    1.10            (case I_Model.is_notyet_input ctxt ppc all ori' pbt of
    1.11              ("",itm)  => itm
    1.12 @@ -178,12 +178,12 @@
    1.13    let
    1.14      val thy = ThyC.get_theory dI
    1.15      val its_ = map (fstr2itm_ thy pbt) selcts (*([1],true,"#Given",Cor (...))*)
    1.16 -    val its = O_Model.add_id its_ 
    1.17 +    val its = O_Model.add_enumerate its_ 
    1.18    in map flattup2 its end
    1.19  
    1.20  (* WN.11.03 for input_icalhd, ~ specify_additem for Add_Given/_Find/_Relation
    1.21     appl_add': generate 1 item 
    1.22 -   appl_add' . is_known: parse, get data from oris (vats, all (elems if list)..)
    1.23 +   appl_add' . contains: parse, get data from oris (vats, all (elems if list)..)
    1.24     appl_add' . is_notyet_input: compare with items in model already input
    1.25     insert_ppc': insert this 1 item*)
    1.26  fun appl_adds dI [] _ pbt selcts = unknown_expl dI pbt selcts
    1.27 @@ -234,8 +234,9 @@
    1.28                    else
    1.29  		                let val pbt = (#ppc o Problem.from_store) pI
    1.30  			                val dI' = #1 (References.select ospec spec)
    1.31 -			                val oris = if pI = #2 ospec then oris 
    1.32 -				                         else O_Model.init fmz_(ThyC.get_theory"Isac_Knowledge") pbt(* |> #1*);
    1.33 +			                val oris =
    1.34 +			                  if pI = #2 ospec then oris 
    1.35 +				                else O_Model.init (ThyC.get_theory "Isac_Knowledge") fmz_ pbt(* |> #1*);
    1.36  		                in (Pos.Pbl, appl_adds dI' oris probl pbt 
    1.37  				              (map itms2fstr probl), meth) end 
    1.38               else if mI <> smI (*FIXME.WN0311: what if probl is incomplete?!*)