1.1 --- a/test/Tools/isac/Knowledge/polyeq-1.sml Mon Apr 06 11:44:36 2020 +0200
1.2 +++ b/test/Tools/isac/Knowledge/polyeq-1.sml Wed Apr 08 12:32:51 2020 +0200
1.3 @@ -374,7 +374,7 @@
1.4 e_metID = get_obj g_metID pt (par_pblobj pt p) (*false*);
1.5 val thy' = get_obj g_domID pt (par_pblobj pt p);
1.6 val (is, sc) = resume_prog thy' (p,p_) pt;
1.7 - val d = e_rls;
1.8 + val d = Rule_Set.empty;
1.9 (*locate_input_tactic (thy',srls) m (pt,(p,p_)) (sc,d) is;
1.10 WAS: not-found-in-program: NotLocatable from Term_Val1 (Const ("List...*)
1.11 "~~~~~ fun locate_input_tactic, args:"; val () = ();