test/Tools/isac/Knowledge/polyeq-1.sml
changeset 59898 68883c046963
parent 59871 82428ca0d23e
child 59900 4e6fc3336336
     1.1 --- a/test/Tools/isac/Knowledge/polyeq-1.sml	Tue Apr 21 12:26:08 2020 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/polyeq-1.sml	Tue Apr 21 15:42:50 2020 +0200
     1.3 @@ -371,7 +371,7 @@
     1.4  (*solve m (pt, pos);
     1.5    WAS: not-found-in-program: NotLocatable from Term_Val1 (Const ("List...*)
     1.6  "~~~~~ fun Step_Solve.by_tactic , args:"; val (m, (pt, po as (p,p_))) = (m, (pt, pos));
     1.7 -e_metID = get_obj g_metID pt (par_pblobj pt p) (*false*);
     1.8 +Spec.e_metID = get_obj g_metID pt (par_pblobj pt p) (*false*);
     1.9          val thy' = get_obj g_domID pt (par_pblobj pt p);
    1.10  	        val (is, sc) = resume_prog thy' (p,p_) pt;
    1.11  		        val d = Rule_Set.empty;