test/Tools/isac/OLDTESTS/root-equ.sml
changeset 59807 c384f7ab263d
parent 59791 0db869a16f83
child 59819 74ad911c10b9
     1.1 --- a/test/Tools/isac/OLDTESTS/root-equ.sml	Sun Feb 16 16:26:05 2020 +0100
     1.2 +++ b/test/Tools/isac/OLDTESTS/root-equ.sml	Thu Feb 20 11:55:29 2020 +0100
     1.3 @@ -558,13 +558,13 @@
     1.4        val pp = par_pblobj pt p;
     1.5        val metID = get_obj g_metID pt pp;
     1.6        val sc = (#scr o get_met) metID;
     1.7 -      val is = get_istate pt (p,p_);
     1.8 +      val is = get_istate_LI pt (p,p_);
     1.9        val thy' = get_obj g_domID pt pp;
    1.10        val thy = assoc_thy thy';
    1.11        val d = e_rls;
    1.12      val Steps [(m',f',pt',p',c',s')] = 
    1.13  	     locate_input_tactic thy' m  (pt,(p,p_)) (sc,d) is;
    1.14 -         val is' = get_istate pt' p';
    1.15 +         val is' = get_istate_LI pt' p';
    1.16  	 LI.find_next_step thy' sc (pt'(*'*),p') is' (*as (ist, ctxt) ---> ist ctxt*);  
    1.17  
    1.18