diff -r 178869f0f4ba -r be30fa5a7b76 test/Tools/isac/Knowledge/polyeq-1.sml
--- a/test/Tools/isac/Knowledge/polyeq-1.sml	Sat Nov 16 17:13:52 2019 +0100
+++ b/test/Tools/isac/Knowledge/polyeq-1.sml	Sat Nov 16 17:46:08 2019 +0100
@@ -199,17 +199,17 @@
 (*TODO simplify assumptions (sqrt!) and check ERROR in has_degree_in*);
 member op = specsteps mI (*false*);
 (*loc_solve_ (mI,m) ptp;
-  WAS: not-found-in-script: NotLocatable from NasNap (Const ("List...*)
+  WAS: not-found-in-script: NotLocatable from Skip1 (Const ("List...*)
 "~~~~~ fun loc_solve_, args:"; val (m, (pt,pos)) = ((mI,m), ptp);
 (*solve m (pt, pos);
-  WAS: not-found-in-script: NotLocatable from NasNap (Const ("List...*)
+  WAS: not-found-in-script: NotLocatable from Skip1 (Const ("List...*)
 "~~~~~ fun solve, args:"; val ((mI,m), (pt, po as (p,p_))) = (m, (pt, pos));
 e_metID = get_obj g_metID pt (par_pblobj pt p) (*false*);
         val thy' = get_obj g_domID pt (par_pblobj pt p);
 	        val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
 		        val d = e_rls;
 (*locate_input_tactic (thy',srls) m  (pt,(p,p_)) (sc,d) is;
-  WAS: not-found-in-script: NotLocatable from NasNap (Const ("List...*)
+  WAS: not-found-in-script: NotLocatable from Skip1 (Const ("List...*)
 "~~~~~ fun locate_input_tactic, args:"; val () = ();
 (*----- outcommented during cleanup of args in lucas-interpreter.sml ------------------------\\* )
 l = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*false*);
@@ -221,7 +221,7 @@
 val up = drop_last l;
   term2str (go up sc);
   (go up sc);
-(*WAS val NasNap _ = scan_up1 ys ((E,up,a,v,S,b),ss) (go up sc)
+(*WAS val Skip1 _ = scan_up1 ys ((E,up,a,v,S,b),ss) (go up sc)
       ... ???? ... is correct*)
 "~~~~~ fun scan_up1, args:"; val ((ys as (y,ctxt,s,Prog sc,d)), (is as (E,l,a,v,S,b),ss), 
 	   (Const ("HOL.Let",_) $ _)) = (ys, ((E,up,a,v,S,b),ss:step list), (go up sc));