diff -r a474900d5bd2 -r 255c853ea2f0 test/Tools/isac/Interpret/mathengine.sml
--- a/test/Tools/isac/Interpret/mathengine.sml	Thu Dec 22 11:12:18 2016 +0100
+++ b/test/Tools/isac/Interpret/mathengine.sml	Thu Dec 22 11:36:20 2016 +0100
@@ -63,7 +63,7 @@
 FROM val oris = prep_ori...
 TO   val (oris, _) = prep_ori...
 *)
-"----- insert ctxt in ptree";
+"----- insert ctxt in ctree";
 (* datatype ppobj
 FROM loc   : istate option * istate option,
 TO   loc   : (istate * ctxt) option * (istate * ctxt) option,
@@ -497,7 +497,7 @@
 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
-"~~~~~ fun me, args:"; val (((_,tac):tac'_), (p:pos'), (_:NEW(*remove*)), (pt:ptree)) = 
+"~~~~~ fun me, args:"; val (((_,tac):tac'_), (p:pos'), (_:NEW(*remove*)), (pt:ctree)) = 
                             (nxt, p, [], pt);
 val ("ok", (_, _, ptp))  = locatetac tac (pt,p)
 val (pt, p) = ptp;
@@ -546,7 +546,7 @@
 "tracing bottom up"; dI = "Build_Inverse_Z_Transform"; (*WAS true*)
     cas = NONE; (*true*)
 	      val hdl = pblterm dI pI;
-        val (pt, _) = cappend_problem e_ptree [] (e_istate, pctxt) (fmz, (dI, pI, mI))
+        val (pt, _) = cappend_problem e_ctree [] (e_istate, pctxt) (fmz, (dI, pI, mI))
 				  (pors, (dI, pI, mI), hdl)
         val pt = update_ctxt pt [] pctxt;
 
@@ -604,7 +604,7 @@
 	        (*                   ^^^^^^^^^^^^^^ in test/../mathengine.sml*)
 	        (* in pt'': tac = Rewrite ("rnorm_equation_add", "Test.rnorm_equation_add")},
                                                            ^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
-"~~~~~ fun complete_solve, args:"; val (auto, c, (ptp as (_, p as (_,p_)): ptree * pos')) =
+"~~~~~ fun complete_solve, args:"; val (auto, c, (ptp as (_, p as (_,p_)): ctree * pos')) =
   (CompleteSubpbl, [], (pt',pos'));
 p = ([], Res) = false;
 member op = [Pbl,Met] p_ = false;
@@ -617,7 +617,7 @@
 	        val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
 	        val (tac_,is,(t,_)) = next_tac (thy',srls) (pt,pos) sc is;
 (*tac_ = Rewrite' (..., ("rnorm_equation_add", "Test.rnorm_equation_add"), ...) !!!!!!!!!!!!!!!!*)
-"~~~~~ fun next_tac, args:"; val (thy, (ptp as (pt, pos as (p, _)):ptree * pos'), 
+"~~~~~ fun next_tac, args:"; val (thy, (ptp as (pt, pos as (p, _)):ctree * pos'), 
   (sc as Prog (h $ body)), (ScrState (E,l,a,v,s,b), ctxt)) = ((thy',srls), (pt,pos), sc, is);
 l = [] = false;
 nstep_up thy ptp sc E l Skip_ a v (*--> Appy (Rewrite' (.., (.., "Test.rnorm_equation_add"), ...)
@@ -651,7 +651,7 @@
 existpt p pt andalso is_empty_tac (get_obj g_tac pt p) = false;
 apfst (append_atomic p ist_res f r f' s) (cut_tree pt (p,Frm));
 apfst : ('a -> 'b) -> 'a * 'c -> 'b * 'c;
-(append_atomic p ist_res f r f' s) : ptree -> ptree;
+(append_atomic p ist_res f r f' s) : ctree -> ctree;
 ;
 (* HERE THE ERROR OCCURED IN THE FIRST APPROACH
   getTactic 1 ([1,1],Frm); <ERROR> syserror in getTactic </ERROR>  <<<<<=========================*)