test/Tools/isac/Knowledge/polyeq-1.sml
changeset 59717 cc83c55e1c1c
parent 59712 be2ffb0248de
child 59718 bc4b000caa39
     1.1 --- a/test/Tools/isac/Knowledge/polyeq-1.sml	Thu Nov 21 12:05:56 2019 +0100
     1.2 +++ b/test/Tools/isac/Knowledge/polyeq-1.sml	Thu Nov 21 15:31:32 2019 +0100
     1.3 @@ -236,7 +236,7 @@
     1.4        ... Ackn_Tac1 ... is correct*)
     1.5  "~~~~~ 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.6       ((((y,s),d),Aundef), ((E, l@[R,D], a,v,S,b),ss), body);
     1.7 -val (a', STac stac) = handle_leaf "locate" thy' sr (E, (a, v)) t
     1.8 +val (a', Program.Tac stac) = handle_leaf "locate" thy' sr (E, (a, v)) t
     1.9               val ctxt = get_ctxt pt (p,p_)
    1.10               val p' = lev_on p : pos;
    1.11  (* WAS val NotAss = associate pt d (m, stac)