1.1 --- a/test/Tools/isac/Knowledge/polyeq-1.sml	Thu Dec 19 12:40:17 2019 +0100
     1.2 +++ b/test/Tools/isac/Knowledge/polyeq-1.sml	Thu Dec 19 16:41:57 2019 +0100
     1.3 @@ -182,7 +182,7 @@
     1.4  
     1.5  (*[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + -1 * sqrt (9 / 16) / 2] TODO sqrt*)
     1.6  val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt =..,Check_elementwise "Assumptions")*)
     1.7 -"~~~~~ fun me, args:"; val ((_,tac), (p:pos'), _, (pt:ctree)) = (nxt, p, [], pt);
     1.8 +"~~~~~ fun me, args:"; val (tac, (p:pos'), _, (pt:ctree)) = (nxt, p, [], pt);
     1.9  "~~~~~ fun locatetac, args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, p));
    1.10  val (mI,m) = mk_tac'_ tac;
    1.11  val Appl m = applicable_in p pt m;
    1.12 @@ -200,10 +200,10 @@
    1.13  member op = specsteps mI (*false*);
    1.14  (*loc_solve_ (mI,m) ptp;
    1.15    WAS: not-found-in-script: NotLocatable from Term_Val1 (Const ("List...*)
    1.16 -"~~~~~ fun loc_solve_, args:"; val (m, (pt,pos)) = ((mI,m), ptp);
    1.17 +"~~~~~ fun loc_solve_, args:"; val (m, (pt,pos)) = (m, ptp);
    1.18  (*solve m (pt, pos);
    1.19    WAS: not-found-in-script: NotLocatable from Term_Val1 (Const ("List...*)
    1.20 -"~~~~~ fun solve, args:"; val ((mI,m), (pt, po as (p,p_))) = (m, (pt, pos));
    1.21 +"~~~~~ fun solve, args:"; val (m, (pt, po as (p,p_))) = (m, (pt, pos));
    1.22  e_metID = get_obj g_metID pt (par_pblobj pt p) (*false*);
    1.23          val thy' = get_obj g_domID pt (par_pblobj pt p);
    1.24  	        val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;