test/Tools/isac/OLDTESTS/root-equ.sml
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