1.1 --- a/test/Tools/isac/Knowledge/polyeq-1.sml	Thu Nov 21 15:31:32 2019 +0100
     1.2 +++ b/test/Tools/isac/Knowledge/polyeq-1.sml	Mon Nov 25 16:39:52 2019 +0100
     1.3 @@ -214,7 +214,7 @@
     1.4  (*----- outcommented during cleanup of args in lucas-interpreter.sml ------------------------\\* )
     1.5  l = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*false*);
     1.6  (*WAS val Reject_Tac1 _ =(go_scan_up1 (thy',srls,scr,d) ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])]) )
     1.7 -  ... Ackn_Tac1 ... is correct*)
     1.8 +  ... Accept_Tac1 ... is correct*)
     1.9  "~~~~~ and go_scan_up1, args:"; val ((ys as (_,_,_,Prog sc,_)), ((E,l,a,v,S,b),ss)) =
    1.10     ((thy',ctxt,srls,scr,d), ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])]));
    1.11  1 < length l (*true*);
    1.12 @@ -232,11 +232,11 @@
    1.13  (*Type error ...: Can't unify _a to pos * pos_ (Incompatible types)*)
    1.14  val [(tac_, mout, ctree, pos', xxx)] = ss;
    1.15  val ss = [(tac_, mout, ctree, pos', []:(pos * pos_) list)];
    1.16 -(*WAS val Reject_Tac1 iss = scan_dn1 (((y,s),d),Aundef) ((E, l@[R,D], a,v,S,b),ss) body
    1.17 -      ... Ackn_Tac1 ... is correct*)
    1.18 +(*WAS val Reject_Tac1 iss = scan_dn1 (((y,s),d),ORundef) ((E, l@[R,D], a,v,S,b),ss) body
    1.19 +      ... Accept_Tac1 ... is correct*)
    1.20  "~~~~~ fun scan_dn1, args:"; val ((((thy',sr),d),ap), (is as (E,l,a,v,S,b), (m,_,pt,(p,p_),c)::ss), t) =
    1.21 -     ((((y,s),d),Aundef), ((E, l@[R,D], a,v,S,b),ss), body);
    1.22 -val (a', Program.Tac stac) = handle_leaf "locate" thy' sr (E, (a, v)) t
    1.23 +     ((((y,s),d),ORundef), ((E, l@[R,D], a,v,S,b),ss), body);
    1.24 +val (a', Program.Tac stac) = interpret_leaf "locate" thy' sr (E, (a, v)) t
    1.25               val ctxt = get_ctxt pt (p,p_)
    1.26               val p' = lev_on p : pos;
    1.27  (* WAS val NotAss = associate pt d (m, stac)