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