1.1 --- a/test/Tools/isac/Knowledge/polyeq-1.sml	Fri Dec 20 09:57:45 2019 +0100
     1.2 +++ b/test/Tools/isac/Knowledge/polyeq-1.sml	Fri Dec 20 10:24:52 2019 +0100
     1.3 @@ -184,7 +184,7 @@
     1.4  val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt =..,Check_elementwise "Assumptions")*)
     1.5  "~~~~~ fun me, args:"; val (tac, (p:pos'), _, (pt:ctree)) = (nxt, p, [], pt);
     1.6  "~~~~~ fun locatetac, args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, p));
     1.7 -val Appl m = applicable_in p pt m;
     1.8 +val Appl m = applicable_in p pt tac;
     1.9  val Check_elementwise' (trm1, str, (trm2, trms)) = m;
    1.10  term2str trm1 = "[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + -1 * sqrt (9 / 16) / 2]";
    1.11  str = "Assumptions";
    1.12 @@ -196,7 +196,7 @@
    1.13    "\"lhs (-1 / 8 + -1 * (1 / 8 + -1 * sqrt (9 / 16) / 2) / 4 +\n     (1 / 8 + -1 * sqrt (9 / 16) / 2) ^^^ 2 =\n     0) is_poly_in 1 / 8 + -1 * sqrt (9 / 16) / 2\","^
    1.14    "\"lhs (-1 / 8 + -1 * (1 / 8 + -1 * sqrt (9 / 16) / 2) / 4 +\n     (1 / 8 + -1 * sqrt (9 / 16) / 2) ^^^ 2 =\n     0) has_degree_in 1 / 8 + -1 * sqrt (9 / 16) / 2 =\n2\"]";
    1.15  (*TODO simplify assumptions (sqrt!) and check ERROR in has_degree_in*);
    1.16 -member op = specsteps mI (*false*);
    1.17 +      (*if*) Tactic.for_specify' m; (*false*)
    1.18  (*loc_solve_ (mI,m) ptp;
    1.19    WAS: not-found-in-script: NotLocatable from Term_Val1 (Const ("List...*)
    1.20  "~~~~~ fun loc_solve_, args:"; val (m, (pt,pos)) = (m, ptp);