1.1 --- a/src/Tools/isac/Interpret/solve.sml	Thu Dec 22 11:12:18 2016 +0100
     1.2 +++ b/src/Tools/isac/Interpret/solve.sml	Thu Dec 22 11:36:20 2016 +0100
     1.3 @@ -90,7 +90,7 @@
     1.4  
     1.5  
     1.6  
     1.7 -type squ = ptree; (* TODO: safe etc. *)
     1.8 +type squ = ctree; (* TODO: safe etc. *)
     1.9  
    1.10  (*13.9.02--------------
    1.11  type ctr = (loc * pos) list;
    1.12 @@ -144,7 +144,7 @@
    1.13  (* val ("Apply_Method",Apply_Method' (mI,_))=(mI,m);
    1.14     val (("Apply_Method",Apply_Method' (mI,_,_)),pt, pos as (p,_))=(m,pt, pos);
    1.15     *)
    1.16 -fun solve ("Apply_Method", m as Apply_Method' (mI, _, _, _)) (pt:ptree, (pos as (p,_))) =
    1.17 +fun solve ("Apply_Method", m as Apply_Method' (mI, _, _, _)) (pt:ctree, (pos as (p,_))) =
    1.18        let val {srls, ...} = Specify.get_met mI;
    1.19          val PblObj {meth=itms, ...} = get_obj I pt p;
    1.20          val thy' = get_obj g_domID pt p;
    1.21 @@ -234,7 +234,7 @@
    1.22          val pr as (p',_) = (lev_up p, Res)
    1.23  	      val pp = par_pblobj pt p
    1.24  	      val r = (fst o (get_obj g_result pt)) p' 
    1.25 -	      (*Rewrite_Set* done at Detail_Set*: this result is already in ptree*)
    1.26 +	      (*Rewrite_Set* done at Detail_Set*: this result is already in ctree*)
    1.27  	      val thy' = get_obj g_domID pt pp
    1.28  	      val (srls, is, sc) = Lucin.from_pblobj' thy' pr pt
    1.29  	      val (tac_,is',_) = Lucin.next_tac (thy',srls) (pt,pr) sc is
    1.30 @@ -274,7 +274,7 @@
    1.31  
    1.32  (*FIXME.WN050821 compare fun solve ... fun nxt_solv*)
    1.33  (* nxt_solv (Apply_Method'     vvv FIXME: get args in applicable_in *)
    1.34 -fun nxt_solv (Apply_Method' (mI,_,_,_)) _ (pt:ptree, pos as (p,_)) =
    1.35 +fun nxt_solv (Apply_Method' (mI,_,_,_)) _ (pt:ctree, pos as (p,_)) =
    1.36        let
    1.37          val {srls,ppc,...} = Specify.get_met mI;
    1.38          val PblObj{meth=itms,origin=(oris,_,_),probl, ...} = get_obj I pt p;
    1.39 @@ -354,7 +354,7 @@
    1.40  	      val (pos',c,_,pt) = Generate.generate1 (assoc_thy "Isac") tac_ is pos pt;
    1.41        in ([(Lucin.tac_2tac tac_, tac_, (pos,is))], c, (pt, pos')) end
    1.42  
    1.43 -(* find the next tac from the script, nxt_solv will update the ptree *)
    1.44 +(* find the next tac from the script, nxt_solv will update the ctree *)
    1.45  and nxt_solve_ (ptp as (pt, pos as (p,p_))) =
    1.46        if e_metID = get_obj g_metID pt (par_pblobj pt p)
    1.47        then ([], [], (pt, (p, p_))) : Chead.calcstate'
    1.48 @@ -390,7 +390,7 @@
    1.49    | autoord CompleteSubpbl = 5
    1.50    | autoord CompleteCalc = 6;
    1.51  
    1.52 -fun complete_solve auto c (ptp as (_, p as (_,p_)): ptree * pos') =
    1.53 +fun complete_solve auto c (ptp as (_, p as (_,p_)): ctree * pos') =
    1.54    if p = ([], Res)
    1.55    then ("end-of-calculation", [], ptp)
    1.56    else
    1.57 @@ -420,7 +420,7 @@
    1.58  	        else complete_solve auto (c @ c') ptp'
    1.59  	    | (_, c', ptp') => complete_solve auto (c @ c') ptp'
    1.60  
    1.61 -and all_solve auto c (ptp as (pt, pos as (p,_)): ptree * pos') = 
    1.62 +and all_solve auto c (ptp as (pt, pos as (p,_)): ctree * pos') = 
    1.63    let
    1.64      val (_,_,mI) = get_obj g_spec pt p
    1.65      val ctxt = get_ctxt pt pos