1.1 --- a/src/Tools/isac/Specify/generate.sml	Fri Apr 10 12:28:47 2020 +0200
     1.2 +++ b/src/Tools/isac/Specify/generate.sml	Fri Apr 10 14:46:55 2020 +0200
     1.3 @@ -11,7 +11,7 @@
     1.4    datatype mout =
     1.5      EmptyMout
     1.6    | Error' of string
     1.7 -  | FormKF of UnparseC.cterm'
     1.8 +  | FormKF of TermC.as_string
     1.9    | PpcKF of pblmet * Model.item Model.ppc
    1.10    | RefinedKF of Celem.pblID * (Model.itm list * (bool * term) list)
    1.11    val generate1 : Tactic.T -> Istate_Def.T * Proof.context -> Calc.T
    1.12 @@ -24,7 +24,7 @@
    1.13      theory -> Tactic.T -> Pos.pos' -> Ctree.ctree -> Pos.pos' * Pos.pos' list * mout * Ctree.ctree
    1.14    val generate : (Tactic.input * Tactic.T * (Pos.pos' * (Istate_Def.T * Proof.context))) list ->
    1.15      Ctree.ctree * Pos.pos' list * Pos.pos' -> Ctree.ctree * Pos.pos' list * Pos.pos' (* for mathengine.sml *)
    1.16 -  val generate_inconsistent_rew : Selem.subs option * ThmC.thm'' -> term -> Istate_Def.T * Proof.context ->
    1.17 +  val generate_inconsistent_rew : Selem.subs option * ThmC_Def.thm'' -> term -> Istate_Def.T * Proof.context ->
    1.18      Pos.pos' -> Ctree.ctree -> Calc.T (* for interface.sml *)
    1.19  (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
    1.20    val tacis2str : taci list -> string
    1.21 @@ -96,8 +96,8 @@
    1.22  (*3.5.00: TODO: foppFK eliminated in interface FE-KE !!!*)
    1.23  datatype foppFK =                  (* in DG cases div 2 *)
    1.24    EmptyFoppFK         (*DG internal*)
    1.25 -| FormFK of UnparseC.cterm'
    1.26 -| PpcFK of UnparseC.cterm' Model.ppc
    1.27 +| FormFK of TermC.as_string
    1.28 +| PpcFK of TermC.as_string Model.ppc
    1.29  fun foppFK2str (FormFK ct') ="FormFK " ^ ct'
    1.30    | foppFK2str (PpcFK  ppc) ="PpcFK " ^ Model.ppc2str ppc
    1.31    | foppFK2str EmptyFoppFK  ="EmptyFoppFK"
    1.32 @@ -118,7 +118,7 @@
    1.33  
    1.34  datatype inout = (*FIXME.WN1105 drop this: was required for proto0 with dialog in sml*)
    1.35    Error_ of string                                                         (*<--*)
    1.36 -| FormKF of cellID * edit * indent * nest * UnparseC.cterm'                   (*<--*)
    1.37 +| FormKF of cellID * edit * indent * nest * TermC.as_string                   (*<--*)
    1.38  | PpcKF of cellID * edit * indent * nest * (pblmet * Model.item Model.ppc) (*<--*)
    1.39  | RefineKF of Stool.match list                                             (*<--*)
    1.40  | RefinedKF of (Celem.pblID * ((Model.itm list) * ((bool * term) list)))   (*<--*)
    1.41 @@ -127,7 +127,7 @@
    1.42    datatype mout = EmptyMout | Error' of inout | Form' of inout | Problems of inout
    1.43  *)
    1.44  datatype mout =
    1.45 -  FormKF of UnparseC.cterm'
    1.46 +  FormKF of TermC.as_string
    1.47  | PpcKF of (pblmet * Model.item Model.ppc) 
    1.48  | RefinedKF of Celem.pblID * (Model.itm list * (bool * term) list)
    1.49  | Error' of string