1.1 --- a/test/Tools/isac/Minisubpbl/530-error-Check_Elementwise.sml	Wed Dec 05 15:29:36 2012 +0100
     1.2 +++ b/test/Tools/isac/Minisubpbl/530-error-Check_Elementwise.sml	Wed Dec 05 15:56:38 2012 +0100
     1.3 @@ -55,19 +55,19 @@
     1.4  "~~~~~ fun nxt_solve_, args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
     1.5  val thy' = get_obj g_domID pt (par_pblobj pt p);
     1.6  val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt; (*is: which ctxt?*)
     1.7 -"~~~~~ fun next_tac, args:"; val (thy, (ptp as (pt, pos as (p, _)):ptree * pos'), (sc as Script (h $ body)),
     1.8 +"~~~~~ fun next_tac, args:"; val (thy, (ptp as (pt, pos as (p, _)):ptree * pos'), (sc as Prog (h $ body)),
     1.9  (ScrState (E,l,a,v,s,b), ctxt)) = ((thy',srls), (pt,pos), sc, is);
    1.10  val ctxt = get_ctxt pt pos
    1.11  val SOME t = parseNEW ctxt "Check_elementwise [x = 1] {(v_v::real). Assumptions}";
    1.12  l; (*= [R, R, D, L, R]*)
    1.13 -"~~~~~ fun nstep_up, args:"; val (thy, ptp, (Script sc), E, l, ay, a, v) =
    1.14 +"~~~~~ fun nstep_up, args:"; val (thy, ptp, (Prog sc), E, l, ay, a, v) =
    1.15  (thy, ptp, sc, E, l, Skip_, a, v);
    1.16  1 < length l; (*true*)
    1.17  val up = drop_last l;
    1.18  go up sc; (* = Const ("HOL.Let", *)
    1.19 -"~~~~~ fun nxt_up, args:"; val (thy, ptp, (scr as (Script sc)), E, l, ay,
    1.20 +"~~~~~ fun nxt_up, args:"; val (thy, ptp, (scr as (Prog sc)), E, l, ay,
    1.21  (t as Const ("HOL.Let",_) $ _), a, v) =
    1.22 -(thy, ptp, (Script sc), E, up, ay, (go up sc), a, v);
    1.23 +(thy, ptp, (Prog sc), E, up, ay, (go up sc), a, v);
    1.24  ay = Napp_; (*false*)
    1.25  val up = drop_last l;
    1.26  val (Const ("HOL.Let",_) $ e $ (Abs (i,T,body))) = go up sc;