changeset 59723 | 2b26d0882d4f |
parent 59686 | 3ce3d089bd64 |
child 59743 | e6d97ceba3fc |
1.1 --- a/test/Tools/isac/OLDTESTS/root-equ.sml Wed Nov 27 18:47:26 2019 +0100 1.2 +++ b/test/Tools/isac/OLDTESTS/root-equ.sml Fri Nov 29 15:22:29 2019 +0100 1.3 @@ -565,7 +565,7 @@ 1.4 val Steps [(m',f',pt',p',c',s')] = 1.5 locate_input_tactic thy' m (pt,(p,p_)) (sc,d) is; 1.6 val is' = get_istate pt' p'; 1.7 - determine_next_tactic thy' (pt'(*'*),p') sc is'; 1.8 + determine_next_tactic thy' sc (pt'(*'*),p') is' (*as (ist, ctxt) ---> ist ctxt*); 1.9 1.10 1.11