1.1 --- a/src/Tools/isac/Specify/input-calchead.sml	Wed Apr 15 11:37:43 2020 +0200
     1.2 +++ b/src/Tools/isac/Specify/input-calchead.sml	Wed Apr 15 13:47:56 2020 +0200
     1.3 @@ -140,7 +140,7 @@
     1.4      in itm end
     1.5      handle _ => (i, v, false, f, Model.Syn (UnparseC.term TermC.empty (*t  ..(t) has not been declared*))))
     1.6    | parsitm dI (itm as (_, _, _, _, Model.Par _)) = 
     1.7 -    error ("parsitm (" ^ Model.itm2str_ (ThyC.thy2ctxt dI) itm ^ "): Par should be internal");
     1.8 +    error ("parsitm (" ^ Model.itm2str_ (ThyC.to_ctxt dI) itm ^ "): Par should be internal");
     1.9  
    1.10  (*separate a list to a pair of elements that do NOT satisfy the predicate,
    1.11   and of elements that satisfy the predicate, i.e. (false, true)*)
    1.12 @@ -162,7 +162,7 @@
    1.13  (* WN.9.11.03 copied from fun appl_add *)
    1.14  fun appl_add' dI oris ppc pbt (sel, ct) = 
    1.15    let 
    1.16 -     val ctxt = Celem.assoc_thy dI |> ThyC.thy2ctxt;
    1.17 +     val ctxt = Celem.assoc_thy dI |> ThyC.to_ctxt;
    1.18    in
    1.19      case TermC.parseNEW ctxt ct of
    1.20  	    NONE => (0, [], false, sel, Model.Syn ct)
    1.21 @@ -224,7 +224,7 @@
    1.22      else oris2itms pbt vat os
    1.23  
    1.24  fun par2fstr (_, _, _, f, Model.Par s) = (f, s)
    1.25 -  | par2fstr itm = error ("par2fstr: called with " ^ Model.itm2str_ (ThyC.thy2ctxt' "Isac_Knowledge") itm)
    1.26 +  | par2fstr itm = error ("par2fstr: called with " ^ Model.itm2str_ (ThyC.id_to_ctxt "Isac_Knowledge") itm)
    1.27  fun itms2fstr (_, _, _, f, Model.Cor ((d, ts), _)) = (f, Model.comp_dts'' (d, ts))
    1.28    | itms2fstr (_, _, _, f, Model.Syn str) = (f, str)
    1.29    | itms2fstr (_, _, _, f, Model.Typ str) = (f, str)
    1.30 @@ -232,7 +232,7 @@
    1.31    | itms2fstr (_, _, _, f, Model.Sup (d, ts)) = (f, Model.comp_dts'' (d, ts))
    1.32    | itms2fstr (_, _, _, f, Model.Mis (d, t)) = (f, UnparseC.term (d $ t))
    1.33    | itms2fstr (itm as (_, _, _, _, Model.Par _)) = 
    1.34 -    error ("parsitm (" ^ Model.itm2str_ (ThyC.thy2ctxt' "Isac_Knowledge") itm ^ "): Par should be internal");
    1.35 +    error ("parsitm (" ^ Model.itm2str_ (ThyC.id_to_ctxt "Isac_Knowledge") itm ^ "): Par should be internal");
    1.36  
    1.37  fun imodel2fstr iitems = 
    1.38    let