diff -r a474900d5bd2 -r 255c853ea2f0 src/Tools/isac/Interpret/solve.sml
--- a/src/Tools/isac/Interpret/solve.sml	Thu Dec 22 11:12:18 2016 +0100
+++ b/src/Tools/isac/Interpret/solve.sml	Thu Dec 22 11:36:20 2016 +0100
@@ -90,7 +90,7 @@
 
 
 
-type squ = ptree; (* TODO: safe etc. *)
+type squ = ctree; (* TODO: safe etc. *)
 
 (*13.9.02--------------
 type ctr = (loc * pos) list;
@@ -144,7 +144,7 @@
 (* val ("Apply_Method",Apply_Method' (mI,_))=(mI,m);
    val (("Apply_Method",Apply_Method' (mI,_,_)),pt, pos as (p,_))=(m,pt, pos);
    *)
-fun solve ("Apply_Method", m as Apply_Method' (mI, _, _, _)) (pt:ptree, (pos as (p,_))) =
+fun solve ("Apply_Method", m as Apply_Method' (mI, _, _, _)) (pt:ctree, (pos as (p,_))) =
       let val {srls, ...} = Specify.get_met mI;
         val PblObj {meth=itms, ...} = get_obj I pt p;
         val thy' = get_obj g_domID pt p;
@@ -234,7 +234,7 @@
         val pr as (p',_) = (lev_up p, Res)
 	      val pp = par_pblobj pt p
 	      val r = (fst o (get_obj g_result pt)) p' 
-	      (*Rewrite_Set* done at Detail_Set*: this result is already in ptree*)
+	      (*Rewrite_Set* done at Detail_Set*: this result is already in ctree*)
 	      val thy' = get_obj g_domID pt pp
 	      val (srls, is, sc) = Lucin.from_pblobj' thy' pr pt
 	      val (tac_,is',_) = Lucin.next_tac (thy',srls) (pt,pr) sc is
@@ -274,7 +274,7 @@
 
 (*FIXME.WN050821 compare fun solve ... fun nxt_solv*)
 (* nxt_solv (Apply_Method'     vvv FIXME: get args in applicable_in *)
-fun nxt_solv (Apply_Method' (mI,_,_,_)) _ (pt:ptree, pos as (p,_)) =
+fun nxt_solv (Apply_Method' (mI,_,_,_)) _ (pt:ctree, pos as (p,_)) =
       let
         val {srls,ppc,...} = Specify.get_met mI;
         val PblObj{meth=itms,origin=(oris,_,_),probl, ...} = get_obj I pt p;
@@ -354,7 +354,7 @@
 	      val (pos',c,_,pt) = Generate.generate1 (assoc_thy "Isac") tac_ is pos pt;
       in ([(Lucin.tac_2tac tac_, tac_, (pos,is))], c, (pt, pos')) end
 
-(* find the next tac from the script, nxt_solv will update the ptree *)
+(* find the next tac from the script, nxt_solv will update the ctree *)
 and nxt_solve_ (ptp as (pt, pos as (p,p_))) =
       if e_metID = get_obj g_metID pt (par_pblobj pt p)
       then ([], [], (pt, (p, p_))) : Chead.calcstate'
@@ -390,7 +390,7 @@
   | autoord CompleteSubpbl = 5
   | autoord CompleteCalc = 6;
 
-fun complete_solve auto c (ptp as (_, p as (_,p_)): ptree * pos') =
+fun complete_solve auto c (ptp as (_, p as (_,p_)): ctree * pos') =
   if p = ([], Res)
   then ("end-of-calculation", [], ptp)
   else
@@ -420,7 +420,7 @@
 	        else complete_solve auto (c @ c') ptp'
 	    | (_, c', ptp') => complete_solve auto (c @ c') ptp'
 
-and all_solve auto c (ptp as (pt, pos as (p,_)): ptree * pos') = 
+and all_solve auto c (ptp as (pt, pos as (p,_)): ctree * pos') = 
   let
     val (_,_,mI) = get_obj g_spec pt p
     val ctxt = get_ctxt pt pos