diff -r a474900d5bd2 -r 255c853ea2f0 test/Tools/isac/Interpret/script.sml
--- a/test/Tools/isac/Interpret/script.sml	Thu Dec 22 11:12:18 2016 +0100
+++ b/test/Tools/isac/Interpret/script.sml	Thu Dec 22 11:36:20 2016 +0100
@@ -231,9 +231,9 @@
 member op = specsteps mI; (*false*)
 (*loc_solve_ (mI,m) ptp; (*Argument: (mI, m) : string * tac Reason: Can't unify tac_ with tac*)*)
 loc_solve_; (*without _ ??? result is -> lOc writing error ???*)
-(*val it = fn: string * tac_ -> ptree * (pos * pos_) -> lOc_*)
+(*val it = fn: string * tac_ -> ctree * (pos * pos_) -> lOc_*)
 (mI,m); (*string * tac*)
-ptp (*ptree * pos'*);
+ptp (*ctree * pos'*);
 "~~~~~ fun loc_solve_, args:"; val (m ,(pt,pos)) = ((mI,m), ptp);
 (*val (msg, cs') = solve m (pt, pos);
 (*Argument: m : string * tac Reason: Can't unify tac_ with tac (Different type constructors)*)*)
@@ -315,7 +315,7 @@
                                  (*WAS stac2tac_ TODO: no match for SubProblem*)
 val thy' = get_obj g_domID pt (par_pblobj pt p);
 val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
-"~~~~~ fun next_tac, args:"; val (thy, (ptp as (pt,(p,_)):ptree * pos'), (sc as Prog (h $ body)), 
+"~~~~~ fun next_tac, args:"; val (thy, (ptp as (pt,(p,_)):ctree * pos'), (sc as Prog (h $ body)), 
 	                               (ScrState (E,l,a,v,s,b), ctxt)) = ((thy',srls), (pt,pos), sc, is);
 l; (*= [R, L, R, L, R, R]*)
 val Appy (m', scrst as (_,_,_,v,_,_)) = nstep_up thy ptp sc E l Skip_ a v;
@@ -348,7 +348,7 @@
           | _ => error "integrate.sml -- me method [diff,integration] -- spec";
 "----- step 8: returns nxt = Rewrite_Set_Inst ([\"(bdv, x)\"],\"integration\")";
 
-"~~~~~ fun me, args:"; val (((_,tac):tac'_), (p:pos'), _, (pt:ptree)) = (nxt, p, c, pt);
+"~~~~~ fun me, args:"; val (((_,tac):tac'_), (p:pos'), _, (pt:ctree)) = (nxt, p, c, pt);
 "~~~~~ fun locatetac, args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));
 val (mI,m) = mk_tac'_ tac;
 val Appl m = applicable_in p pt m;
@@ -366,7 +366,7 @@
 ini = NONE; (*true*)
             val (m', (is', ctxt'), _) = next_tac (thy', srls) (pt, (p, Res)) sc (is, ctxt);
 	            val d = e_rls (*FIXME: get simplifier from domID*);
-"~~~~~ fun locate_gen, args:"; val ((ts as (thy',srls)), (m:tac_), ((pt,p):ptree * pos'), 
+"~~~~~ fun locate_gen, args:"; val ((ts as (thy',srls)), (m:tac_), ((pt,p):ctree * pos'), 
 	                     (scr as Prog (h $ body),d), (ScrState (E,l,a,v,S,b), ctxt)) = 
                    ((thy',srls), m', (pt,(p, Res)), (sc,d), (is', ctxt'));
 val thy = assoc_thy thy';