changeset 59790 | a1944acd8dcf |
parent 59772 | d6bab1992c6a |
child 59791 | 0db869a16f83 |
1.1 --- a/test/Tools/isac/OLDTESTS/root-equ.sml Tue Feb 04 16:45:36 2020 +0100 1.2 +++ b/test/Tools/isac/OLDTESTS/root-equ.sml Tue Feb 04 17:11:54 2020 +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 - LucinNEW.find_next_step thy' sc (pt'(*'*),p') is' (*as (ist, ctxt) ---> ist ctxt*); 1.8 + Lucin.find_next_step thy' sc (pt'(*'*),p') is' (*as (ist, ctxt) ---> ist ctxt*); 1.9 1.10 1.11