1.1 --- a/src/Tools/isac/Specify/input-calchead.sml	Thu Apr 09 17:16:48 2020 +0200
     1.2 +++ b/src/Tools/isac/Specify/input-calchead.sml	Thu Apr 09 18:21:09 2020 +0200
     1.3 @@ -5,9 +5,9 @@
     1.4  
     1.5  signature INPUT_CALCHEAD =
     1.6  sig
     1.7 -  datatype iitem = Find of Rule.cterm' list | Given of Rule.cterm' list | Relate of Rule.cterm' list
     1.8 +  datatype iitem = Find of UnparseC.cterm' list | Given of UnparseC.cterm' list | Relate of UnparseC.cterm' list
     1.9    type imodel = iitem list
    1.10 -  type icalhd = Pos.pos' * Rule.cterm' * imodel * Pos.pos_ * Celem.spec
    1.11 +  type icalhd = Pos.pos' * UnparseC.cterm' * imodel * Pos.pos_ * Celem.spec
    1.12    val input_icalhd : Ctree.ctree -> icalhd -> Ctree.ctree * Ctree.ocalhd
    1.13    val cas_input : term -> (Ctree.ctree * Ctree.ocalhd) option
    1.14  (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
    1.15 @@ -87,23 +87,23 @@
    1.16  (*** handle an input calc-head ***)
    1.17  
    1.18  datatype iitem = 
    1.19 -  Given of Rule.cterm' list
    1.20 +  Given of UnparseC.cterm' list
    1.21  (*Where is never input*) 
    1.22 -| Find  of Rule.cterm' list
    1.23 -| Relate  of Rule.cterm' list
    1.24 +| Find  of UnparseC.cterm' list
    1.25 +| Relate  of UnparseC.cterm' list
    1.26  
    1.27  type imodel = iitem list
    1.28  
    1.29  (*calc-head as input*)
    1.30  type icalhd =
    1.31    Pos.pos' *     (*the position of the calc-head in the calc-tree*) 
    1.32 -  Rule.cterm' *   (*the headline*)
    1.33 +  UnparseC.cterm' *   (*the headline*)
    1.34    imodel *         (*the model (without Find) of the calc-head*)
    1.35    Pos.pos_ *     (*model belongs to Pbl or Met*)
    1.36    Celem.spec;      (*specification: domID, pblID, metID*)
    1.37  val e_icalhd = (Pos.e_pos', "", [Given [""]], Pos.Pbl, Celem.e_spec)
    1.38  
    1.39 -fun is_casinput (hdf : Rule.cterm') ((fmz_, spec) : Selem.fmz) =
    1.40 +fun is_casinput (hdf : UnparseC.cterm') ((fmz_, spec) : Selem.fmz) =
    1.41    hdf <> "" andalso fmz_ = [] andalso spec = Celem.e_spec
    1.42  
    1.43  (* re-parse itms with a new thy and prepare for checking with ori list *)