diff -r a474900d5bd2 -r 255c853ea2f0 test/Tools/isac/Knowledge/polyeq.sml
--- a/test/Tools/isac/Knowledge/polyeq.sml	Thu Dec 22 11:12:18 2016 +0100
+++ b/test/Tools/isac/Knowledge/polyeq.sml	Thu Dec 22 11:36:20 2016 +0100
@@ -166,7 +166,7 @@
 val (p,_,f,nxt,_,pt) = me nxt p [] pt;         
 (*[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + -1 * sqrt (9 / 16) / 2] TODO sqrt*)
 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt =..,Check_elementwise "Assumptions")*)
-"~~~~~ fun me, args:"; val ((_,tac), (p:pos'), _, (pt:ptree)) = (nxt, p, [], pt);
+"~~~~~ fun me, args:"; val ((_,tac), (p:pos'), _, (pt:ctree)) = (nxt, p, [], 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;
@@ -194,7 +194,7 @@
 		        val d = e_rls;
 (*locate_gen (thy',srls) m  (pt,(p,p_)) (sc,d) is;
   WAS: not-found-in-script: NotLocatable from NasNap (Const ("List...*)
-"~~~~~ 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,p_)) ,(sc,d) ,is); (* locate_gen 2nd pattern *)
 val thy = assoc_thy thy';
@@ -216,8 +216,8 @@
       val i = mk_Free (i, T);
       val E = upd_env E (i, v);
 (*Type error ...: Can't unify _a to pos * pos_ (Incompatible types)*)
-val [(tac_, mout, ptree, pos', xxx)] = ss;
-val ss = [(tac_, mout, ptree, pos', []:(pos * pos_) list)];
+val [(tac_, mout, ctree, pos', xxx)] = ss;
+val ss = [(tac_, mout, ctree, pos', []:(pos * pos_) list)];
 (*WAS val NasApp iss = assy (((y,s),d),Aundef) ((E, l@[R,D], a,v,S,b),ss) body
       ... Assoc ... is correct*)
 "~~~~~ fun assy, args:"; val ((((thy',sr),d),ap), (is as (E,l,a,v,S,b), (m,_,pt,(p,p_),c)::ss), t) =