test/Tools/isac/OLDTESTS/root-equ.sml
changeset 59559 f25ce1922b60
parent 59497 8952c43fdce3
child 59592 99c8d2ff63eb
     1.1 --- a/test/Tools/isac/OLDTESTS/root-equ.sml	Tue Jun 25 10:46:20 2019 +0200
     1.2 +++ b/test/Tools/isac/OLDTESTS/root-equ.sml	Tue Jun 25 12:48:24 2019 +0200
     1.3 @@ -566,9 +566,9 @@
     1.4        val thy = assoc_thy thy';
     1.5        val d = e_rls;
     1.6      val Steps [(m',f',pt',p',c',s')] = 
     1.7 -	     locate_gen thy' m  (pt,(p,p_)) (sc,d) is;
     1.8 +	     locate_input_tactic thy' m  (pt,(p,p_)) (sc,d) is;
     1.9           val is' = get_istate pt' p';
    1.10 -	 next_tac thy' (pt'(*'*),p') sc is';  
    1.11 +	 determine_next_tactic thy' (pt'(*'*),p') sc is';  
    1.12  
    1.13  
    1.14