1.1 --- a/test/Tools/isac/Knowledge/polyeq-1.sml	Tue Mar 31 14:05:10 2020 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/polyeq-1.sml	Tue Mar 31 15:43:33 2020 +0200
     1.3 @@ -238,8 +238,8 @@
     1.4  val (Program.Tac stac, a') = check_leaf "locate" thy' sr (E, (a, v)) t
     1.5               val ctxt = get_ctxt pt (p,p_)
     1.6               val p' = lev_on p : pos;
     1.7 -(* WAS val NotAss = associate pt d (m, stac)
     1.8 -      ... Ass ... is correct*)
     1.9 +(* WAS val Not_Associated = associate pt d (m, stac)
    1.10 +      ... Associated ... is correct*)
    1.11  "~~~~~ fun associate, args:"; val (pt, _, (m as Check_elementwise' (consts,_,(consts_chkd,_))),
    1.12      (Const ("Prog_Tac.Check'_elementwise",_) $ consts' $ _)) = (pt, d, m, stac);
    1.13  term2str consts;
    1.14 @@ -267,7 +267,7 @@
    1.15    ([2],Res)  []      Check_elementwise "Assumptions"*)
    1.16  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    1.17  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    1.18 -val asm = get_assumptions_ pt p;
    1.19 +val asm = Ctree.get_assumptions pt p;
    1.20  if f2str f = "[]" andalso 
    1.21    terms2str asm = "[\"lhs (2 + -1 * x + x ^^^ 2 = 0) is_poly_in x\"," ^
    1.22      "\"lhs (2 + -1 * x + x ^^^ 2 = 0) has_degree_in x = 2\"]" then ()