1867 (id, string_of_thmI thm), f,(e_term,[(*!?!8.6.03*)])), |
1867 (id, string_of_thmI thm), f,(e_term,[(*!?!8.6.03*)])), |
1868 Uistate, (e_term, Sundef))) (*next stac*) |
1868 Uistate, (e_term, Sundef))) (*next stac*) |
1869 |
1869 |
1870 (* val(thy, ptp as (pt,(p,_)), sc as Script (h $ body),ScrState (E,l,a,v,s,b))= |
1870 (* val(thy, ptp as (pt,(p,_)), sc as Script (h $ body),ScrState (E,l,a,v,s,b))= |
1871 ((thy',srls), (pt,pos), sc, is); |
1871 ((thy',srls), (pt,pos), sc, is); |
1872 *) |
1872 *) |
1873 | next_tac thy (ptp as (pt,(p,_)):ptree * pos') (sc as Script (h $ body)) |
1873 | next_tac thy (ptp as (pt,(p,_)):ptree * pos') (sc as Script (h $ body)) |
1874 (ScrState (E,l,a,v,s,b)) = |
1874 (ScrState (E,l,a,v,s,b)) = |
1875 ((*writeln("### next_tac-----------------: E= "); |
1875 ((*writeln("### next_tac-----------------: E= "); |
1876 writeln( istate2str (ScrState (E,l,a,v,s,b)));*) |
1876 writeln( istate2str (ScrState (E,l,a,v,s,b)));*) |
1877 case if l=[] then appy thy ptp E [R] body None e_term |
1877 case if l=[] then appy thy ptp E [R] body None v |
1878 else nstep_up thy ptp sc E l Skip_ a v of |
1878 else nstep_up thy ptp sc E l Skip_ a v of |
1879 Skip (v,_) => (*finished*) |
1879 Skip (v,_) => (*finished*) |
1880 (case par_pbl_det pt p of |
1880 (case par_pbl_det pt p of |
1881 (true, p', _) => |
1881 (true, p', _) => |
1882 let val (_,pblID,_) = get_obj g_spec pt p'; |
1882 let val (_,pblID,_) = get_obj g_spec pt p'; |