1.1 --- a/src/sml/ME/script.sml	Fri Nov 03 14:30:32 2006 +0100
     1.2 +++ b/src/sml/ME/script.sml	Fri Nov 03 18:15:55 2006 +0100
     1.3 @@ -1869,12 +1869,12 @@
     1.4  
     1.5  (* val(thy, ptp as (pt,(p,_)), sc as Script (h $ body),ScrState (E,l,a,v,s,b))=
     1.6        ((thy',srls), (pt,pos),  sc,                     is);
     1.7 - *)
     1.8 +   *)
     1.9    | next_tac thy (ptp as (pt,(p,_)):ptree * pos') (sc as Script (h $ body)) 
    1.10  	     (ScrState (E,l,a,v,s,b)) =
    1.11    ((*writeln("### next_tac-----------------: E= ");
    1.12     writeln( istate2str (ScrState (E,l,a,v,s,b)));*)
    1.13 -   case if l=[] then appy thy ptp E [R] body None e_term
    1.14 +   case if l=[] then appy thy ptp E [R] body None v
    1.15         else nstep_up thy ptp sc E l Skip_ a v of
    1.16        Skip (v,_) =>                                              (*finished*)
    1.17        (case par_pbl_det pt p of