test/Tools/isac/Knowledge/polyeq-1.sml
changeset 59831 edf1643edde5
parent 59804 403f00b309ef
child 59844 373d13915f8c
     1.1 --- a/test/Tools/isac/Knowledge/polyeq-1.sml	Wed Mar 18 14:51:58 2020 +0100
     1.2 +++ b/test/Tools/isac/Knowledge/polyeq-1.sml	Wed Mar 18 15:23:15 2020 +0100
     1.3 @@ -205,7 +205,7 @@
     1.4  "~~~~~ fun Step_Solve.by_tactic , args:"; val (m, (pt, po as (p,p_))) = (m, (pt, pos));
     1.5  e_metID = get_obj g_metID pt (par_pblobj pt p) (*false*);
     1.6          val thy' = get_obj g_domID pt (par_pblobj pt p);
     1.7 -	        val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
     1.8 +	        val (is, sc) = resume_prog thy' (p,p_) pt;
     1.9  		        val d = e_rls;
    1.10  (*locate_input_tactic (thy',srls) m  (pt,(p,p_)) (sc,d) is;
    1.11    WAS: not-found-in-script: NotLocatable from Term_Val1 (Const ("List...*)