diff -r a474900d5bd2 -r 255c853ea2f0 test/Tools/isac/Interpret/ctree.sml
--- a/test/Tools/isac/Interpret/ctree.sml	Thu Dec 22 11:12:18 2016 +0100
+++ b/test/Tools/isac/Interpret/ctree.sml	Thu Dec 22 11:36:20 2016 +0100
@@ -13,23 +13,23 @@
 "-------------- fun get_ctxt -------------------------------------";
 "-------------- fun update_ctxt, fun g_ctxt ----------------------";
 "-------------- check positions in miniscript --------------------";
-"-------------- get_allpos' (from ptree above)--------------------";
-"-------------- cut_level (from ptree above)----------------------";
-"-------------- cut_tree (from ptree above)-----------------------";
-"=====new ptree 1a miniscript with mini-subpbl ===================";
+"-------------- get_allpos' (from ctree above)--------------------";
+"-------------- cut_level (from ctree above)----------------------";
+"-------------- cut_tree (from ctree above)-----------------------";
+"=====new ctree 1a miniscript with mini-subpbl ===================";
 "-------------- cut_level ( ,Frm) on Incomplete Nd ---------------";
-"=====new ptree 2 miniscript with mini-subpbl ====================";
-"-------------- cut_tree (intermedi.ptree: 3rd level)-------------";
-"-------------- cappend (from ptree above)------------------------";
+"=====new ctree 2 miniscript with mini-subpbl ====================";
+"-------------- cut_tree (intermedi.ctree: 3rd level)-------------";
+"-------------- cappend (from ctree above)------------------------";
 "-------------- cappend minisubpbl -------------------------------";
-"=====new ptree 3 ================================================";
+"=====new ctree 3 ================================================";
 "-------------- move_dn ------------------------------------------";
 "-------------- move_dn: Frm -> Res ------------------------------";
 "-------------- move_up ------------------------------------------";
 "------ move into detail -----------------------------------------";
-"=====new ptree 3a ===============================================";
+"=====new ctree 3a ===============================================";
 "-------------- move_dn in Incomplete ctree ----------------------";
-"=====new ptree 4: crooked by cut_level_'_ =======================";
+"=====new ctree 4: crooked by cut_level_'_ =======================";
 (*############## development stopped 0501 ########################*)
 (******************************************************************)
 (*              val SAVE_get_trace = get_trace;                   *)
@@ -39,13 +39,13 @@
 (*              val get_trace = SAVE_get_trace;                   *)
 (******************************************************************)
 (*############## development stopped 0501 ########################*)
-"=====new ptree 4 ratequation ====================================";
+"=====new ctree 4 ratequation ====================================";
 "-------------- pt_extract form, tac, asm<>[] --------------------";
-"=====new ptree 5 minisubpbl =====================================";
+"=====new ctree 5 minisubpbl =====================================";
 "-------------- pt_extract form, tac, asm ------------------------";
-"=====new ptree 6 minisubpbl intersteps ==========================";
+"=====new ctree 6 minisubpbl intersteps ==========================";
 "-------------- get_allpos' new ----------------------------------";
-"-------------- cut_tree new (from ptree above)-------------------";
+"-------------- cut_tree new (from ctree above)-------------------";
 "-------------- subst2subs subs2subst sube2subst subte2subst -----";
 "-----------------------------------------------------------------";
 "-----------------------------------------------------------------";
@@ -105,7 +105,7 @@
 
 val cuts = get_allp [] ([], ([],Frm)) pt;
 val cuts2 = get_allps [] [1] (children pt);
-"ctree.sml-------------- cut_tree new (from ptree above)----------";
+"ctree.sml-------------- cut_tree new (from ctree above)----------";
 val (pt', cuts) = cut_tree pt ([1],Frm);
 "ctree.sml-------------- cappend on complete ctree from above ----";
 val (pt', cuts) = cappend_form pt [1] (e_istate, e_ctxt) (str2term "Inform[1]");
@@ -139,9 +139,9 @@
 
  show_pt pt;
 
-"-------------- get_allpos' (from ptree above)--------------------";
-"-------------- get_allpos' (from ptree above)--------------------";
-"-------------- get_allpos' (from ptree above)--------------------";
+"-------------- get_allpos' (from ctree above)--------------------";
+"-------------- get_allpos' (from ctree above)--------------------";
+"-------------- get_allpos' (from ctree above)--------------------";
 if get_allpos' ([], 1) pt = 
    [([], Frm), 
     ([1], Frm), 
@@ -206,9 +206,9 @@
 
 
 
-"-------------- cut_level (from ptree above)----------------------";
-"-------------- cut_level (from ptree above)----------------------";
-"-------------- cut_level (from ptree above)----------------------";
+"-------------- cut_level (from ctree above)----------------------";
+"-------------- cut_level (from ctree above)----------------------";
+"-------------- cut_level (from ctree above)----------------------";
 show_pt pt;
 show_pt pt';
 default_print_depth 99; cuts; default_print_depth 3;
@@ -252,25 +252,25 @@
 	   ([4], Res)]
 then () else error "ctree.sml: diff:behav. in cut_level 2a";
 
-if pr_ptree pr_short pt' = ".    ----- pblobj -----\n1.   x + 1 = 2\n2.   x + 1 + -1 * 2 = 0\n"
+if pr_ctree pr_short pt' = ".    ----- pblobj -----\n1.   x + 1 = 2\n2.   x + 1 + -1 * 2 = 0\n"
 then () else error "ctree.sml: diff:behav. in cut_level 2b";
 
 val (pt',cuts) = cut_level [] [3] pt ([3,1],Frm);
 if cuts = [([3, 1], Res), ([3, 2], Res)]
 then () else error "ctree.sml: diff:behav. in cut_level 3a";
-if pr_ptree pr_short pt' = ".    ----- pblobj -----\n1.   x + 1 = 2\n2.   x + 1 + -1 * 2 = 0\n3.    ----- pblobj -----\n3.1.   -1 + x = 0\n4.   [x = 1]\n"
+if pr_ctree pr_short pt' = ".    ----- pblobj -----\n1.   x + 1 = 2\n2.   x + 1 + -1 * 2 = 0\n3.    ----- pblobj -----\n3.1.   -1 + x = 0\n4.   [x = 1]\n"
 then () else error "ctree.sml: diff:behav. in cut_level 3b";
 
 val (pt',cuts) = cut_level [] [3] pt ([3,1],Res);
 if cuts = [([3, 2], Res)]
 then () else error "ctree.sml: diff:behav. in cut_level 4a";
-if pr_ptree pr_short pt' = ".    ----- pblobj -----\n1.   x + 1 = 2\n2.   x + 1 + -1 * 2 = 0\n3.    ----- pblobj -----\n3.1.   -1 + x = 0\n4.   [x = 1]\n"
+if pr_ctree pr_short pt' = ".    ----- pblobj -----\n1.   x + 1 = 2\n2.   x + 1 + -1 * 2 = 0\n3.    ----- pblobj -----\n3.1.   -1 + x = 0\n4.   [x = 1]\n"
 then () else error "ctree.sml: diff:behav. in cut_level 4b";
 
 
-"-------------- cut_tree (from ptree above)-----------------------";
-"-------------- cut_tree (from ptree above)-----------------------";
-"-------------- cut_tree (from ptree above)-----------------------";
+"-------------- cut_tree (from ctree above)-----------------------";
+"-------------- cut_tree (from ctree above)-----------------------";
+"-------------- cut_tree (from ctree above)-----------------------";
 val (pt', cuts) = cut_tree pt ([2],Frm);(*not created by move_dn -- not on WS*)
 
 (*============ inhibit exn AK110726 ==============================================
@@ -340,9 +340,9 @@
 	   ([], Res)]
 then () else error "ctree.sml: diff:behav. in cut_tree 4";
 
-"=====new ptree 1a miniscript with mini-subpbl ===================";
-"=====new ptree 1a miniscript with mini-subpbl ===================";
-"=====new ptree 1a miniscript with mini-subpbl ===================";
+"=====new ctree 1a miniscript with mini-subpbl ===================";
+"=====new ctree 1a miniscript with mini-subpbl ===================";
+"=====new ctree 1a miniscript with mini-subpbl ===================";
 val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
 val (dI',pI',mI') =
   ("Test",["sqroot-test","univariate","equation","test"],
@@ -383,9 +383,9 @@
 
 
 
-"=====new ptree 2 miniscript with mini-subpbl ====================";
-"=====new ptree 2 miniscript with mini-subpbl ====================";
-"=====new ptree 2 miniscript with mini-subpbl ====================";
+"=====new ctree 2 miniscript with mini-subpbl ====================";
+"=====new ctree 2 miniscript with mini-subpbl ====================";
+"=====new ctree 2 miniscript with mini-subpbl ====================";
 reset_states ();
  CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"], 
    ("Test", ["sqroot-test","univariate","equation","test"],
@@ -401,9 +401,9 @@
 if (term2str o fst) (get_obj g_result pt [3,2,1]) = "x = 0 + 1" then ()
 else error "mini-subpbl interSteps broken";
 
-"-------------- cut_tree (intermedi.ptree: 3rd level)-------------";
-"-------------- cut_tree (intermedi.ptree: 3rd level)-------------";
-"-------------- cut_tree (intermedi.ptree: 3rd level)-------------";
+"-------------- cut_tree (intermedi.ctree: 3rd level)-------------";
+"-------------- cut_tree (intermedi.ctree: 3rd level)-------------";
+"-------------- cut_tree (intermedi.ctree: 3rd level)-------------";
 (*WN050225 intermed. outcommented
  val (pt', cuts) = cut_tree pt ([3,2,1],Frm);
  if cuts = [([3, 2, 1], Res),
@@ -421,9 +421,9 @@
  then () else error "ctree.sml: diff:behav. in cut_tree 3rd level 2";
 
 
-"-------------- cappend (from ptree above)------------------------";
-"-------------- cappend (from ptree above)------------------------";
-"-------------- cappend (from ptree above)------------------------";
+"-------------- cappend (from ctree above)------------------------";
+"-------------- cappend (from ctree above)------------------------";
+"-------------- cappend (from ctree above)------------------------";
 val (pt',cuts) = cappend_form pt [3,2,1] e_istate (str2term "newnew");
 if cuts = [([3, 2, 1], Res),
 	   ([3, 2, 2], Res),
@@ -452,7 +452,7 @@
 "-------------- cappend minisubpbl -------------------------------";
 "-------------- cappend minisubpbl -------------------------------";
 "-------------- cappend minisubpbl -------------------------------";
-"=====new ptree 1 miniscript with mini-subpbl ====================";
+"=====new ctree 1 miniscript with mini-subpbl ====================";
 val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
 val (dI',pI',mI') =
   ("Test",["sqroot-test","univariate","equation","test"],
@@ -550,9 +550,9 @@
 
 WN050225 intermed. outcommented---*)
 
-"=====new ptree 3 ================================================";
-"=====new ptree 3 ================================================";
-"=====new ptree 3 ================================================";
+"=====new ctree 3 ================================================";
+"=====new ctree 3 ================================================";
+"=====new ctree 3 ================================================";
 
 reset_states ();
  CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"], 
@@ -665,9 +665,9 @@
  if p = ([2, 6], Res) then() 
  else error "ctree.sml: diff.behav. in move into detail";
 
-"=====new ptree 3a ===============================================";
-"=====new ptree 3a ===============================================";
-"=====new ptree 3a ===============================================";
+"=====new ctree 3a ===============================================";
+"=====new ctree 3a ===============================================";
+"=====new ctree 3a ===============================================";
  reset_states ();
  CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"], 
    ("Test", ["sqroot-test","univariate","equation","test"],
@@ -698,9 +698,9 @@
 
 
 
-"=====new ptree 4: crooked by cut_level_'_ =======================";
-"=====new ptree 4: crooked by cut_level_'_ =======================";
-"=====new ptree 4: crooked by cut_level_'_ =======================";
+"=====new ctree 4: crooked by cut_level_'_ =======================";
+"=====new ctree 4: crooked by cut_level_'_ =======================";
+"=====new ctree 4: crooked by cut_level_'_ =======================";
 reset_states ();
 CalcTree
 [(["equality (x/(x^2 - 6*x+9) - 1/(x^2 - 3*x) =1/x)",
@@ -733,11 +733,11 @@
 moveActiveFormula 1 ([4,2],Res)(*4.2.1.*);
 interSteps 1 ([4,2],Res)(*..is activeFormula !?!*);
 val ((pt,_),_) = get_calc 1;
-writeln(pr_ptree pr_short pt);
+writeln(pr_ctree pr_short pt);
 (*delete [4,1] in order to make pos [4],[4,4] for pblobjs differen [4],[4,3]:
  ###########################################################################*)
 val (pt, ppp) = cut_level_'_ [] [] pt ([4,1],Frm);
-writeln(pr_ptree pr_short pt);
+writeln(pr_ctree pr_short pt);
 
 
 
@@ -785,7 +785,7 @@
 	 | SOME t => term2str (subst_atomic (mk_env probl) t)
     end;
 *)
-(*.get an 'interval' from ptree down to a certain level
+(*.get an 'interval' from ctree down to a certain level
    by 'take_fromto children' of the nodes with specific 'from' and 'to';
    'i > 0' suppresses output during recursive descent towards 'from'
    b: the 'from' incremented to the actual pos
@@ -820,7 +820,7 @@
     (getnd i             (       b,[0]) [99999] nd) @
     (getnds ~99999 false (lev_on b,[0]) q nds); 
 in
-(*get an 'interval from to' from a ptree as 'intervals f t' of respective nodes
+(*get an 'interval from to' from a ctree as 'intervals f t' of respective nodes
   where 'from' are pos, i.e. a key as int list, 'f' an int (to,t analoguous)
 (1) the 'f' are given 
 (1a) by 'from' if 'f' = the respective element of 'from' (left margin)
@@ -834,7 +834,7 @@
 	(take_fromto (hdp p) (hdq q) (children pt));
 end;
 
-writeln(pr_ptree pr_short pt);
+writeln(pr_ctree pr_short pt);
 
 case get_trace pt [1,3] [4,1,1] of
     [[1,3],[1,4],[2],[3],[4],[4,1],[4,1,1]] => () 
@@ -892,9 +892,9 @@
 (******************************************************************)
 
 
-"=====new ptree 4 ratequation ====================================";
-"=====new ptree 4 ratequation ====================================";
-"=====new ptree 4 ratequation ====================================";
+"=====new ctree 4 ratequation ====================================";
+"=====new ctree 4 ratequation ====================================";
+"=====new ctree 4 ratequation ====================================";
 reset_states ();
 CalcTree
 [(["equality (x/(x^2 - 6*x+9) - 1/(x^2 - 3*x) =1/x)",
@@ -907,12 +907,12 @@
 val (Form f, tac, asms) = pt_extract (pt, p);
 (*============ inhibit exn WN120316 ==============================================
 if term2str f = "[x = 6 / 5]" andalso p = ([], Res) then ()
-  else error "after ===new ptree 4 ratequation ===";
+  else error "after ===new ctree 4 ratequation ===";
 (*WN120317.TODO dropped rateq*)
 ============ inhibit exn WN120316 ==============================================*)
 if p = ([], Res) andalso term2str f = "[]" (*see WN120317.TODO dropped rateq*)
 andalso asms = [] (*STRANGE!, compare test --- x / (x ^ 2 - 6 * x + 9) - 1 / (x ^ 2 ...*)
-then () else error "after ===new ptree 4 ratequation ===";
+then () else error "after ===new ctree 4 ratequation ===";
 
 
 "-------------- pt_extract form, tac, asm<>[] --------------------";
@@ -941,9 +941,9 @@
 
 
 
-"=====new ptree 5 minisubpbl =====================================";
-"=====new ptree 5 minisubpbl =====================================";
-"=====new ptree 5 minisubpbl =====================================";
+"=====new ctree 5 minisubpbl =====================================";
+"=====new ctree 5 minisubpbl =====================================";
+"=====new ctree 5 minisubpbl =====================================";
 reset_states ();
 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"], 
    ("Test", ["sqroot-test","univariate","equation","test"],
@@ -1020,9 +1020,9 @@
   | _ => error "diff.behav.in ctree.sml: pt_extract ([], Res)";
 ========== inhibit exn AK110719 ==============================================*)
 
-"=====new ptree 6 minisubpbl intersteps ==========================";
-"=====new ptree 6 minisubpbl intersteps ==========================";
-"=====new ptree 6 minisubpbl intersteps ==========================";
+"=====new ctree 6 minisubpbl intersteps ==========================";
+"=====new ctree 6 minisubpbl intersteps ==========================";
+"=====new ctree 6 minisubpbl intersteps ==========================";
 reset_states ();
 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"], 
    ("Test", ["sqroot-test","univariate","equation","test"],
@@ -1117,9 +1117,9 @@
 
 
 (**#################################################################**)
-"-------------- cut_tree new (from ptree above)-------------------";
-"-------------- cut_tree new (from ptree above)-------------------";
-"-------------- cut_tree new (from ptree above)-------------------";
+"-------------- cut_tree new (from ctree above)-------------------";
+"-------------- cut_tree new (from ctree above)-------------------";
+"-------------- cut_tree new (from ctree above)-------------------";
 show_pt pt;
 val b = get_obj g_branch pt [];
 if b = TransitiveB then () else