test/Tools/isac/Knowledge/polyeq-1.sml
changeset 59852 ea7e6679080e
parent 59851 4dd533681fef
child 59861 65ec9f679c3f
     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 () = ();