1.1 --- a/src/Tools/isac/MathEngBasic/ctree-basic.sml	Mon Dec 30 11:16:00 2019 +0100
     1.2 +++ b/src/Tools/isac/MathEngBasic/ctree-basic.sml	Wed Jan 15 11:47:38 2020 +0100
     1.3 @@ -22,7 +22,7 @@
     1.4    datatype ppobj =
     1.5      PblObj of
     1.6       {branch: branch,
     1.7 -      cell: Celem.lrd option,
     1.8 +      cell: TermC.lrd option,
     1.9        loc: (Istate_Def.T * Proof.context) option * (Istate_Def.T * Proof.context) option,
    1.10        ostate: ostate,
    1.11        result: Selem.result,
    1.12 @@ -36,7 +36,7 @@
    1.13        env: (Istate_Def.T * Proof.context) option}
    1.14    | PrfObj of
    1.15       {branch: branch,
    1.16 -      cell: Celem.lrd option,
    1.17 +      cell: TermC.lrd option,
    1.18        loc: (Istate_Def.T * Proof.context) option * (Istate_Def.T * Proof.context) option,
    1.19        ostate: ostate,
    1.20        result: Selem.result,
    1.21 @@ -172,7 +172,7 @@
    1.22  (* executed tactics (tac_s) with local environment etc.;
    1.23    used for continuing eval script + for generate *)
    1.24  type ets =
    1.25 -  (Celem.path *(* of tactic in scr, tactic (weakly) associated with tac_                   *)
    1.26 +  (TermC.path *(* of tactic in scr, tactic (weakly) associated with tac_                   *)
    1.27     (Tactic.T * (* (for generate)                                                           *)
    1.28      Env.T *      (* with 'tactic=result' as  rule, tactic ev. _not_ ready for 'parallel let' *)
    1.29      Env.T *      (* with results of (ready) tacs                                             *)
    1.30 @@ -182,7 +182,7 @@
    1.31    list;
    1.32  
    1.33  fun ets2s (l,(m,eno,env,iar,res,s)) = 
    1.34 -  "\n(" ^ Celem.path2str l ^ ",(" ^ Tactic.string_of m ^
    1.35 +  "\n(" ^ TermC.path2str l ^ ",(" ^ Tactic.string_of m ^
    1.36    ",\n  ens= " ^ Env.subst2str eno ^
    1.37    ",\n  env= " ^ Env.subst2str env ^
    1.38    ",\n  iar= " ^ Rule.term2str iar ^
    1.39 @@ -198,7 +198,7 @@
    1.40  
    1.41  datatype ppobj = (* TODO: arrange according to signature *)
    1.42    PrfObj of 
    1.43 -   {cell  : Celem.lrd option, (* where in form tac has been applied, FIXME.WN0607 rename field *)
    1.44 +   {cell  : TermC.lrd option, (* where in form tac has been applied, FIXME.WN0607 rename field *)
    1.45  	  form  : term,             (* where tac is applied to                                       *)
    1.46  	  tac   : Tactic.input,           (* also in istate                                                *)
    1.47  	  loc   : (Istate_Def.T *   (* script interpreter state                                      *)
    1.48 @@ -212,7 +212,7 @@
    1.49  	  result: Selem.result,     (* result and assumptions                                        *)
    1.50  	  ostate: ostate}           (* Complete <=> result is OK                                     *)
    1.51  | PblObj of 
    1.52 -   {cell  : Celem.lrd option, (* unused: meaningful only for some _Prf_Obj                     *)
    1.53 +   {cell  : TermC.lrd option, (* unused: meaningful only for some _Prf_Obj                     *)
    1.54      fmz   : Selem.fmz,        (* from init:FIXME never use this spec;-drop                     *)
    1.55      origin: (Model.ori list) *(* representation from fmz+pbt+met
    1.56                                   for efficiently adding items in probl, meth                   *)